First-Order Logic & Satisfiability Modulo Theories | Formal Methods

[00:00:04]okay so welcome back everyone to the fall methods for softw engineering lecture and today we're starting a new topic so the last lecture uh didn't happen because of the holiday but uh today we're starting a new thing and that's called satisfiability modular Theory um so as you remember we have those kind of four chapters we completed now the sub solving but we're still working on the homework some of you I'm not sure did anybody already submit the homework no okay so that's uh yeah I think next week uh June next week right uh Friday next week or something like that yeah great um yeah so today we'll start a new topic um and we will look at what we have learned so far we have learned s solving and we we know what s solving is based on what kind of language we can use what logic we can use to express our problems we can express them in this propositional logic um yeah in the in this logic proposition logic where we have variables that are just Atomic propositions or Boolean variables that can be true or false and um there might be things that we cannot easily encode in as a sub problem because we cannot easily express them in um propositional logic so can you give maybe some examples of what could it be that we cannot yet handle so this lecture doesn't stop with SS solving it continues right uh so what is it that might be missing right does anybody remember things that we can express inside we had these like natural language descriptions that we could translate to well statements logical statements that we could translate and then check whether one statement follows from other statements right that's something we could do then Ro based Access Control we could check parts of it right um feature models we could analyze them using S um so here are some examples well we have one example uh why we are here yeah that's uh difficult to encode in s um why is that so I'm yeah why is it difficult to encode I mean in general all these tools that we're looking at um a why is very difficult right uh so maybe we would have to concretize this here or something like that right but even even if we have um a question of let's say why can I not include this product in or or this feature in my product um this is a separate story and and there there are works on the why question or formal analysis they probably will still not answer why we here here um but yeah um and I'm afraid that also the other tools that we're going to go through they will not be able to answer this question um any more things we cannot express in sat or we cannot easily express in sat okay so let's look at some examples and see if we can encode them in sat if sat is so powerful maybe we can encode them so here is a logic puzzle it's just logic so we should be able it's it's similar to this uh um what was his name was it Paul who missed the train was it Tony who was it at the train station and there were no taxis at the train station then he might be late for his meeting John it was John yeah okay so John is not in this but there are other people in this so here um we have the dreber Mansion mystery Someone who lived in dread Berry Mansion killed Aunt Agatha and Agatha the Butler and Charles were the only people who lived in dread Berry Mansion a killer always hates their victim so we have a bunch of statements about some people right we have only three people Agatha the Butler and Charles um then a killer always hates their victim and is never richer than their victim so it's a madeup setting but uh you you can see that it involves some maybe Rel between people right so there are some maybe special things like killer so this is probably one of maybe one of those if those were the only ones there right maybe one of them is the the the one who killed Aunt Agatha um and then there are some more information we know about these people so Charles hates no one that Aunt Agatha hates so there's some relation again between Charles and Agatha um Agatha hates everyone except the butler the butler hates everyone not richer than Aunt Agatha the butler also hates everyone Agatha hates no one hates everyone and Agatha is not the butler so who killed and Agatha um okay let's encode this inide how would you encode this inside so if we if we think back at other encodings that we did right we had the encoding of the uh Ro based access we had the encoding of uh the feature models the first thing we had to think about is what are the variables so uh in the role based access we said that the variables might be uh the the roles and the capabilities or well um maybe just the yeah so which role do you have and what capabilities then should you have and then we wrote some predicates around around these um in the feature models we decided that the um features will be the variables because they either there or not there either included or not included um so what would be the variables uh in this puzzle now okay so so you could consider uh H and okay but uh this ah okay so I think it's I think we can we can maybe ignore this that Agatha is not the butler we can also say that Charles is not the butler let's say those are really three separate people Agatha the Butler and Charles they're all separate people this is a bit stronger than this last or the previous to last Point here which just says that Agata is not the butler let's say uh the butler is its own person so then this makes it slightly simpler um yeah but how do we encode stuff like uh who's richer if you if you have richer as variables um according to the third statement was the richest okay because she died and the Vic must be poor than kill or at least she's richer than the one who killed her yeah okay but how do we express that she's richer than the one who killed her if we you only have Boolean variables so actually the information that we know is true is a bit more composed of multiple things right it's not only that someone is richer than someone else we know that uh um some killer is never richer than their victim so we have to relate killer and victim in this kind of richer thing so how many combinations could we have when we have agath the Butler and Charles we have three people so we could probably relate three people each to each so it's nine possible combinations so we have nine Boolean variables for who is richer than who else so we could have a Boolean variable saying um Agatha is richer than Agatha we could have one that says Agatha is richer than the butler we could have one Agatha is richer than Charles right so for this richer we would need then well nine variables um for hating how many do we need again nine variables right because that's again a relation between people um and we know something about these variables right so we know Agatha hates everyone except the butler so we know that some of these variables are true some are false and then we write this down as constraints uh do we have other things that we need to express in variables so we have nine variables for richer nine variables for uh hating do we have other things that we would need to express in variables how do we reason about uh being the killer being the killer yeah so how many how do we relate being the killer how many people could be the killer three again so we have uh because that's now what's the difference between hating and being the killer why do we only need three variables for being the Killer and nine variables for encoding hating can okay yeah because every person can be a killer or not but it only relates to a single person right hating relates to two people so that's the big difference that we have some kind of things that relate multiple people and then we need we kind of blow up the variables because it's the number of people times the number of people if we would have something that relates to three people uh yeah three people then it would be uh 3 * 3 * 3 so we would already have 27 bullan variables so yeah now how many other relation we had the hates relation we had the uh richer relation we had the kills relation um that's maybe it don't know and then we have a lot of constraints that we have to write right each one of those we have to uh encode okay um yeah that's maybe a possibility but maybe not the nicest one right uh we have one answer is that somebody who didn't answer okay assigning the rules and expressing the dependency and solve so we we basically uh yeah these roles like whether somebody is uh yeah the roles or maybe the relations between the people right and then the dependencies are maybe the constraints that we know uh so we could probably encode this in s but it would mean we have a lot of variables and we probably have quite a few constraints on these variables um okay and well after this encoding in these variables how do we know who killed aath we check satisfiability we get hopefully a solution an assignment and this assignment gives us one killer safies well we have three variables for killer we have like Agatha is the killer Butler is the killer Charles is the Killer so well one of them or many of them might be true um but actually there's there's something we overlooked um because that they are the killer doesn't mean they killed Agatha or does it mean well I mean here it says uh that wait Someone who lived there killed Agatha um maybe more people are dead I don't know um so actually I would say that that um killed is again a relation between two people well yeah two probably yeah or more uh two I guess would be fine um so we would have even more variables so maybe sat is not the best unless you do it completely programmatically and you don't care how many variables you generate um but doing this manually it's probably not the closest and why is that what's the problem there why do we need so many variables so many possibilities are there there are so many possibilities yes and um so it's a bit like if you if you think about um did anybody ever write assembly code or Machine level code you need many many lines to express some things that in let's say some high level programming language you can express much easier so and and the reason is that maybe some high level concepts are missing in this kind of assmbly language and I would maybe say that sat is like our Assembly Language it has very basic concepts it has this concept of Boolean variables it has well propositional operators on them and or stuff like that but it doesn't have many high LEL Concepts it doesn't have the concept for example of a relation or a predicate between uh so this this hates would be some high level concept could be some high level concept um but s doesn't really have that so maybe we need some other language um and this is a an encoding um that might make it easier so this is an encoding in first order logic and we will look at what is this first order logic so you can have a look at this this is the translation of this puzzle and now we actually have these kind of predicates here we we say there's a predicate killed that relates some person X to some person a and this a would be atha um so and we say there exists some X where X killed atha right and then we have the other ones um we have the hates relation and the richual relation so uh yeah for example um here it would say that Agatha hates Agatha and Agatha hates the well Charles so this is because here it said uh Agatha hates everyone except the butler right so we will not have um hates AB because Agatha doesn't hate the butler but we will have the other ones there okay so this is something um if we could express it in a language which is much closer to the actual way that the problem is formulated this might be nice um so then what about this one uh that's also maybe something you have come across uh some some puzzle about dogs cats and mice so you can spend exactly $100 and you have to buy exactly 100 animals dogs will cost you $15 each cats will cost $1 and mice will cost 25 um so if you have to spend $1100 and you have to buy 100 animals what would be the most simple solution here you can't buy 100 dogs right because that's too much money um you could buy 100 cats right that's one each cat $1 that would fit but it says here you also have to buy at least one of each um so now that gets a bit more tricky and then um how many of each should you buy um yeah anybody has an idea how many of each we should buy uh how do we solve this in in general I mean we we could change the numbers right and it would be a different puzzle so who knows this kind of stuff from school sorry okay so you can basically put some uh arithmetics some mathematical formulas uh on numbers um so you could introduce some symbols here what what is this uh dark cat and mouse thing here what does it stand for it says so that's basically we have to buy at least one dog at least one cat at least one Mouse so this variable dog now is a number and we say this number is the number of dogs that we're going to buy and this has to be greater or equal to one so we have to buy at least one dog one cat one Mouse and then here we can use this same variable but now we can add them up and we say it has to be exactly 100 animals right um and then here we just give the price in cents instead of dollars so a dog would cost us well 1,500 cents which is the $15 um and the the mouse would only be 25 cents and all of them together they should equal our budget of $100 right so um now all we have to do is we have to find some solution and what would this solution look like I mean just just in general it would like what what are we asking for here we are asking for how many of each do we buy so a solution would basically assign a number to each of these right uh probably we want an integer number right we we don't want to buy half a dog right um so it would probably put some integer number to each of of these variables and this would be a solution now how would we do this in s doesn't sound like it's a good idea to encode this in s right because yeah what is missing in s about this variables and S were all Boolean here we want integers then what were the operators that we had in set we had conjunction disjunction stuff like that but here we have plus and multiplication so we have addition multiplication all of these that's all not in set right it makes things uh more challenging uh what about puzzles like this who has ever seen similar puzzles like that yeah so it's basically um these symbols here they are kind of variables um yeah actually when we when we looked at this puzzle last time um it occurred to I don't know maybe one of the students that there might be some um tricky meaning here because this is a rainbow right the question is is this a double rainbow which is its own variable or is this two times this thing which means we we're actually only having the rainbow variable the rain variable and the I don't know lightning variable or do we have the double rainbow variable right so these puzzles they're always not very clear um but that's a different challenge right but still um in sat that's probably not so easy right we we probably want again uh some integer variables and then we have operations between these we have division multiplication and so on uh and we have some equalities here uh like in the previous example we also had these uh like yeah equalities here to say how many it has to be in total so we want something that also can handle math right um at least some kind of math um so now let's look at the second language that we're going to have but um I'm going to warn you because this is really um we're going to build this up in a in a very very formal way because um there are many things that are in this language and um very far on the bottom somewhere there is basically propositional logic and then there's stuff on top of it on top of it on top of it and and we will see that this is an extremely flexible framework that we're going to look at uh so first logic can be very complicated uh we're going to look at it from a formal side and then once we have done this formal side we're going to look at it from again the let's say user perspective um so how are we going to use it to actually encode our problems in this kind of language so it is important to have this background of this formal stuff to know what is going on behind the scenes so that we can see where are the challenges when we're trying to solve problems or when we're trying to translate problems to this language why might it fail uh which are the cases that might work well so um again as with uh well s this thing is not all powerful it can't do all the things we would like it to do the things that we saw on the slides those it can do those examples um but there are there is stuff where it is not that well not working so well so we're going to look at maybe why that is or what might be the limitations yes every problems that we are seeing here can be done Byram why necessary to use a formal method ah so if you how do how would you program these you would maybe iterate through the possible solutions or how would you solve this using programming so like a search problem right many of these tools they they actually can be translated to search problems and um what they do is they have been optimized and made very efficient to deal with this kind of stuff for well maybe decades that people have been working on this so the thing is that if translate your problem to smt and it is really as difficult as smt then the smt solver will very likely be much faster than any of the programs that You' write but a very good observation is if you can do it maybe with a simple algorithm you should do it with a simple algorithm so um that's also what some colleagues are complaining about now that um they have to look at some works that people did and people used S&T solvers and they said well don't use S&T solvers in this setting uh because yes S&T solvers are nice but they're not the solution to everything if you have something that works very very efficient as a normal program write a normal program right but if you have something that is very tricky you don't know a solution you don't have an existing algorithm or uh the complexity of the problem itself is very high the same complexity as smt solvers then probably they will outperform everything that you could write but um yeah if if your problem is not really a complex problem then try to solve it in another way that's the same with uh deep learning now everybody like there's a hype in deep learning everybody tries to solve everything with deep learning even stuff they shouldn't even stuff where there's other more simpler straightforward Solutions but well deep learning is great so let's throw deep learning at everything and yeah don't make this mistake in general uh and and also don't make it with f methods um so you always have to check is this problem really a problem that pays off to translate uh to a formal method or not um and if it exactly fits the for method then you can imagine that probably um the for method has a much better like faster algorithm implemented than you could write from scratch okay so um yeah and we will see in in particular for uh so for for sub solving if you have something where you have to try all the combinations that's basically 2 to the N where n is this number of variables and um I think that some people they they measure empirically what is the um the real like expected complexity of sub solvers and in the worst case of course it's this 2 to the N but uh they said I think it's it's getting close to like 1.2 to the n in in Practical cases so that's like a a much better thing um but still it it has this High complexity so um yeah um and here we will see in S&T solving we will see that there are basically many many add-ons so uh this stuff is arithmetic and arithmetic can be solved very efficient using some specific algorithms and actually smt solvers they will do that we will see what this T stands for that it stands for theories so smt is basically s stands for satisfiability so that's like sat then modulo theories means that we can incorporate some theories and also solve theories on the way that we're solving the sub problem and these theories they have the dedicated solvers so if you have something um like with simple arithmetic it will use an arithmetic solver in the background so it will actually have a whole toolbox of solvers uh and we we call this thing all S&T solver but the SNT solver will actually try to understand okay what's this component of the problem that you're trying to solve and then try to use the dedicated solver for that um so yeah there is um a lot of engineering work in in these tools so um yeah let's have a look the first so this this first order logic um is our second language that we're looking at the first was this propositional logic now it's first order logic and uh we already saw that there is some additional stuff going on so um what we introduced are some functions some variables and some predicates so predicates are sometimes a bit maybe not so obvious so equals could actually be seen as a predicate because it has two parameters um maybe on the left side uh dog plus cat plus something is the left parameter and then on the right side we have the 100 and this predicate is true if and only if left side is 100 and right side is 100 right if they if they are really equal um then based on these we can build some Atomic formulas or literals if you remember we also had something called literals in uh in sat our literals in sat were very very simple um they were basically a an atomic uh variable so an atomic formula like a or b or Q or R and their negation those were our literals when we when we talked about conjunctive normal form we said that we can basically on the innermost thing we only have a variable or it's negation those were our literals here literals are already a bit more complex um but they're always wrapped into predicates so um it evaluates to true or false it internally it can use uh functions and apply them to variables because that's basically what these uh predicates kind of wrap around um but then basically everything that kind of is wrapped in in a predicate that's a literal now so everything that's true or false that's a well yeah inside some predicate it's a literal now then we have some quantifier free formulas um and we have formulas which have quantifiers so basically everything without those quantifiers that's a quantifier free formula um and the quantifiers that we usually have they are this uh for all and exists quantifiers so here we only see the for all quantifiers um but we will go yeah a lot more in detail of how to build up um our our logic so these functions and and variables and predicates they are not arbitrary we have to kind of Define them for our language um so for function symbols we usually have some alphabet and some examples of functions could be f G or a very concrete function the plus um we don't know yet how plus is defined but that's a function right it takes uh usually one thing on the left one thing on the right and it returns a new value so that's a function then predicate symbols uh there are some very simple predicate symbols like true and false um they don't have any parameters We cannot put more stuff in them uh we can't like have true of some X or Y it's just basically like a constant um and we also have an alphabet for these predicates because we need to distinguish what's a function what's a predicate um and then a very important thing is the aity of a function that's basically how many parameters can it take so um yeah if we have t z this means it can't take any parameters then it's a constant right because there's nothing that it takes as as input so it can only be a constant so true false these would be constants um then the notation here used on these slides um if you're not sure about the a t uh you can put this uh like forward slash and then the number of the a so F with this forward SL2 would mean that it has A2 so it can take two parameters and uh then return some value um and then we have a set of variables and these variables are not um in any of our uh functions or predicates right so you can use a variable but you can't use uh a function name for a variable name this would Clash like in any programming language you have those keywords and you can't put your uh or you shouldn't have your your variables as as the keywords for example here the clashes between the function symbols and predicate symbols um and then we can have a set of variables um now let's look at some examples to understand this arity of functions um or the arity of our symbols um yeah so there are some statements about arities um and you should select all the correct ones all the meaningful arties so it says here the number 12 has r0 or the number one has R1 um and remember R was this like how many parameters does it take in in our framework okay so we have some answers um so the number 12 has a zero why is that that's correct why it's a constant yes exactly it doesn't have any parameters so yeah it has a zero uh the number one has R1 no because it's a constant as well so it also has RR zero then the addition function has arity two the plus yes we can take two parameters on the left on the right so aity two yeah the negation function has R2 no because it has a one right we can negate one parameter then the relation whether one person is richer than another person has R2 yes because relates two people uh if you give it two people and says yes one is richer than the other or no one is not richer than or the first is not richer than the second okay yeah so that's about um arities now um the next thing we have is terms and the set of terms is some set formed by these syntax rules so a term is either um some variable or it's a function applied to other terms so yeah very simple and it only works uh yeah for these functions in F so terms we did we wouldn't have any predicates in there right um a term would only be either a variable or function applied to variables now uh well it says function applied to terms does it mean I can Nest functions I can apply a function to a function yes exactly because I can well a function itself is a term so I can plug it in as a term inside another function so I can basically Nest functions I can uh put variables in functions or just have variables themselves okay um and then we can also say a term is ground if it contains no variables um and now let's have a look at ah we don't have an example for terms okay but terms are very very simple right variables or functions applied to variables or ground terms how can we have no variables in a ground term it's a constant if it's a constant yeah so if we have a function that's a constant then it's ground term because we don't have any parameters of it or if we have a function on constants right then it's also fine um okay so there are probably many ground terms that we can uh create so uh yeah if we would have I don't know 1 + one would that be a ground term yes because one is a a constant um yeah and plus is a function so that's a ground term because we don't have any variables but if we would have x + one then X would probably be the variable so yeah this would not be a ground term okay then um yeah Atomic formulas in our language an atom would be defined as has some predicate over terms and um yeah we can say an atom is again ground if it contains no variables so again the same uh thing if if it doesn't contain variables then it's ground uh and then we can say literals are atoms and the negation of atoms okay so just uh wrap some kind of predicate around some terms and then uh you have your Atomic formulas now to build quantifier free formulas then we can take atoms and add our um Boolean logic operators because now why can we apply negation to an atom because an atom is always wrapped in a predicate and a predicate is true or false right that's that's how we can how we can apply these operators here which are defined for uh for our propositional logic we can apply them to these new atoms because now um we can basically our atoms have a Boolean value after the evaluation of the predicates so yeah we have again negation B implication conjunction disjunction and regular implication and again you could just use uh the negation and disjunction to abbreviate all the others but yeah here they all are um and then basically the the highest level of elements that we can express in our logic are first order logic formulas or first order formulas and we can add uh some quantifiers and then we get first order uh formulas so that's basically on top of our uh formulas that we had so far uh our quantifier free formulas we can wrap them in quantifiers and then we have the complete language of our first order formulas um so we have the for all which is the universal quantification and the exists which is the ex existential quantification um and then there's something called free occurrences of variables um are those where the abl are not bound by a quantifier so how does what does a quantifier look like a quantifier always has some kind of variable that it quantifies over um and then this formula here if it's not a ground term then it can have many variables right but if it has for example the variable X in here in this formula then this means that X will have the value that we um used in this quantification here um so X is then bound to this X um but if there are two variables in there for example uh X and Y and we only bind X then Y is still a free variable so it it has yeah it occurs freely inside the formula so uh let's have a look at some examples we have this formula up here for all X for all y uh x and z implies y um I'm not asking you to evaluate it I just want to know which ones are the free variables in this formula so we can look at well how many variables do we have uh X Y and Z so yeah choose which ones are occurring free in this formula so um does X occur freely no because it's in a quantifier so here we have for all X this means that X is not a free variable uh here we have for all y so Y is also not a free variable um so the only free variable is Z then let's have a look at the next one what about this formula now that's a bit tricky for all x x equals y or for all y x and z implies y so now the question is which binds stronger uh did we say which bins stronger no we didn't have the operator precedence to let me let me check do I have it on this no okay uh so let's let's put some parenthesis um now I'm presentation mode I can't easily edit it um so imagine some parentheses here and well some parentheses around this other one as well sorry yeah so that then what would be the free variables where is y free Y is free in this one right uh and here Y is bound is X free in this one X is free in this one right we only quantify over y like if we had this well I I already should put the parenthesis to make it more clear um so if we have this for all X this and or for all y that so if the highlighted thing was again in parenthesis uh then we would have the occurrence of x3 um and z3e and this means that we actually have kind of twice the variable x uh because we have it once bound here but this name only relates to the left part and then we have the variable X here which is now free in this formula um so it's basically another uh variable X you can kind of like in um in in Loops when you Nest variables you can have uh a local variable which has the name of some higher visible variable and it kind of Shadows it so now like in a in a method you can define a variable which actually is a field available in that class and then it will take the locally known name as the one uh that it has that it uses so that's exactly the same here if we have this scope of the for all that goes from this uh for this x then it will take this locally known X here which is bound by this quantifier and here it will take some free x because there not Bound by uh the second quantifier okay um yeah then we we can we call a sentence as a first order formula with no free variables okay but um yeah we will see that the more interesting ones are uh ones with three variables because then we might want to check uh what values we can assign to those free variables to make a formula satisfiable so um yeah but now we have this this kind of syntax right we can now write formulas um so we write our quantifier free formulas and now we extended them with quantifiers right so uh now you can all write first order formulas um but do you know what they mean we have to give them a meaning so to give them a meaning that's called the semantics now for propositional Logic the semantics was really easy because it's either true or false and we know what uh with the truth tables we basically said what it what the semantics are right we said and means that both of them have to be true and so on so there the sematics are quite easy but now uh for um first or the logic we actually have different parts that we can have in our formula we can have those predicates we can have the functions we can have variables so how do we give this thing a meaning how do we make sure that we can evaluate the formulas um for that we need some domain uh which is often also called the universe so it's some set of elements and these elements are uh yeah maybe some some values that we can assign um so the easiest thing is assignments to variables so um this XM that's in our model so um to give the meaning we need models um and our model our interprets variables by assigning them concrete values so the variable X we might assign a concrete value from s so now what might s be this is something we have to say when we give this uh model the model has to Define this the model has to Define what is s so for example for the cats dogs Mouse thing um we would probably take a model where s is the set of integers so s would be then the set of integers then our variables doc cat Mouse we would each one assign a specific integer then um we need to interpret also our functions so we would have to say what actually does plus do um and yeah we probably Define it in the way that we know what plus does right if you have one thing on the left and one thing on the right uh it adds them up right it it gives the sum um but that's not yet defined we have to Define this by giving a concrete function that interprets this plus symbol on the domain of of integers right so of the on this domain that we gave so uh we would then have a function that for example um takes n parameters so plus we said r t is two so it takes two parameters and gives us a third value so it could take one and two as the parameters and it will give us three as the result but that's something uh the model has to give us so this interpretation that's something the model would give us um if it's not from somewhere else we will see that there are for plus standard things we can get them basically bought in from somewhere else but in general that's the semantics uh we have to get interpretations similarly for predicates um the predicate hates uh now ah for for this Agata puzzle what would be the domain s um we said the predicates we have a predicate hates we have a predicate killed we have a predicate richer um but what would be our domain s for this Agatha puzzle three people three people yeah we probably have a set of three people so the domain s would be Agatha Butler and Charles right um and then each predicate so for example the predicate richer would relate uh always tles of people it's it has A2 so it relates maybe Agatha and the butler or Agatha and and Charles right so that's how we would have to give the model will have to give interpretations the model will have to say how does this predicate work when is this predicate true when is this predicate false and it does so by relating the elements from the domain um yeah so we basically give interpretations for functions for predicates and assignments for variables and the the very important thing is this set s right because that has to come from somewhere and we saw that that although it's the same first order logic um the models are completely different right even like in terms of the structure the model for the um dread bar mention puzzle we had the domain as uh three people for the uh dogs cats and mice puzzle we had the domain as integers so yeah and all that is in this first Auto logic okay so a formula is true if uh in some model so let's say we have a formula and we have a model um the uh formula is true in that model if it evaluates to two under the given interpretations over the domain s so basically we apply all these interpretations we replace all those funny symbols uh by their correct interpretations on this one domain that we have and then we check is it true or false right uh and M is a model for some set of sentences T if all sentences of T are true in m so um you can also yeah Define a model for a set of sentences which where those quantifier free no not quantifier free there where the ones without free variables so if everything is completely deter in terms of the variables then um our model can be checked against the different sentences um so yeah sentences they could also then be the different constraints that we want to hold so um yeah and then of course we want this model to satisfy those constraints good so now uh let's yeah look at the semantics of um some terms so a term in a model is interpreted as for each variable we basically interpret it as the uh assignment of the variable right so this x m this X in the model was some concrete value assignment but what do we do with functions well functions um they are interpreted by replacing all the terms by the current interpretations of uh the term so it's like a recursive thing if I want to translate a function that is over terms I have to translate all the terms and I have to replace the function by its interpretation in the model so uh this I don't know plus I have to say well that's actually the function that adds the two numbers okay then uh the predicate the predicate is true if and only if uh the now it's terms so we're still on the kind of syntactic level we replace them with their current interpretation of the term in that's given to us by the model um and then we check whether it is in this concrete predicate that the model defined so this interpretation of the predicate that was uh yeah now some subset of uh value combinations so if we would have something like the uh richer predicate and we have Agatha and the butler then we would have to first go ahead and replace Agatha by actually the Agatha element from the domain s and the butler by the butler element from the domain s um and then we have to check whether they are related in this interpretation of the Richer predicate so that sounds a bit strange because now we have like U on the syntactic level on the term level we have an Agatha and we have an Agatha in the semantics level in this domain s often we can give them let's say the same name we can give them the same symbol but uh yeah in in theory they are actually different um but we don't yeah have to worry about that too much um we just have to know that there is that there needs to be something like this model and that this model has lots of responsibility because it has to say what are actually what's the domain and how do we interpret each of those functions and if we want to um yeah here we said that uh if we want to um a model for a set of sentences so we want a model for a set of constraints then that's what we will ask the smt solare to do so the S&T solare has to come up with all these things it has to give us interpretations and meanings for the well the domain the functions the predicates so um an smt solver has to do a lot more than a sub solver right okay yeah some uh examples or of the basic semantics um we can Define the semantics that's basically our our highest level formulas that we can build so a formula is true in some model if uh the model uh yeah um ah sorry yeah so the negation of a formula would be modeled by m if uh the formula itself is not modeled by m that's the simple interpretation of uh negation and the equivalence or here the B by implication would be modeled by this model if they are both modeled by the model and then for the other ones it's simply um yeah this operator here is only uh so the the conjunction here is only modeled by our model if our model models both of them individually so for or then of course it's enough if one of them is modeled um and so on the tricky bit is then the quantification that's the new part so for all X this formula should hold this means now we have to take the model and replace the occurrence of x uh by some specific value and we have to do this for all the values from the domain so it says for all of them right so if we have some variable in our formula and it's inside a universal quantification then we basically have to check for all the possible um variables if we replace X by Al so sorry for all the possible values in the domain if we replace X by that value is the does the model still model the formula uh so that's for for all and for exists we're just asking is there some value that we can uh replace the X with and then do we get um that the model now models the formula okay um yeah that's this this this variable assignment so we we update the model by saying uh this variable X now needs to point to this specific value s okay um then we can see that proposition logic is actually included in so the subs solving stuff that we had so far with proposition logic uh it's some subset of first order logic we don't have predicates we don't uh really have functions except for constants and um then we just have kind of these operators the quantification we don't even need um so we can build we can build everything that we had in our proposition logic we can build in first order logic right uh and and lots of the stuff that first logic has on top we don't need um yeah and then this uh interpretation here there are no variables so everything should be quite simple so we can just interpret a uh formula then again simply based on these rules and see if we get true or false whether it's really modeled by and that's our um yeah that's our semantics of propositional logic so what we have is truly more than what we had before okay and of course then the domain would usually be this true and false and the constant true we map to the value true and the constant false we map to the value false and um now we would have to assign these variables to some values in s so to satisfy this to make it true we could for example set P false q fals and R false then we have false implies and yeah we don't need to go on because that's already satisfied okay um now if we look back at this thing we see that this was actually already first order logic and now we know what these uh elements all mean we have some predicate symbols um we have some variables X and Y and uh we have some constants here this a was standing for Agatha and that's our constant Agatha B for Butler and C for Charles so those were our constants um then we have these predicates here killed hates richer um and those are our yeah constraints on those symbols that we have introduced now what would it look like if we want a model for this we need a domain right I mean you you already mentioned it right the domain would have to be would have to have some values right so it would be those three values of the Agatha batler Charles um then of course the interpretation of the variable or of the sorry of the constant a should be this Agatha from that Set uh C should of course map to that set in our domain so now this a is different from that a because this a is the uh constant in our formula and this a is uh the value in the domain that our model provides right um yeah and richer could be mapped for example to this predicate that only relates b and a which would mean that only the butler is richer than Agatha but uh yeah that's not necessarily conforming to all those constraints so these are just examples uh and of course what we wanted to figure out is what like element what value might there be in this interpretation of killed where a is on the right side so who killed Agatha that was the original question so the Yeah question mark is what what do we need to do to find uh that concrete assignment so here this is not a complete model because we have these kind of incomplete things in there right so uh or it's not a model that would uh model our formula okay um now that we have all these building blocks there's actually some additional stuff that we need because we don't want to always Define what do these functions mean uh we we want to have like some kind of library of existing functions of stuff that we know stuff that we want to reuse um right now we said uh well equality is some kind of predicate but how is that defined we would have to Define it each time we want to give a model right and I ideally we would hope that everybody defines equality the same way right but how can we be sure if everybody uh can Define equality from scratch in their model this would be very confusing if like we Define different kinds of equality and then um they might even contradict right so we don't want that um so the the trick that we can do is we can add some theories the theories what we will see is um they will basically are they they always work over some signature so the signature is the stuff that has the function names that has the predicate names uh and it's a set of sentences or axioms so it's a set of things that has to hold over our um yeah over uh over our signatures so a set of uh properties that our signatures need to have um and what we capture is the intended interpretation of the functions and predicates in the signature so we have usually plus we want this to be addition we don't want plus to be anything else so that's our intended interpretation of plus and to capture what does plus mean we can put that into a theory or that this zero thing is actually the number zero these are things that we need to put in theories because so far in this first order logic nobody ever said anything like that we just had those um predicate names and we had the function names but we we never gave them any meaning so we want some fixed meaning and that's why we add some theories so um you could also say that uh the theory uh you can view some kind of first order Theory as the class of all models because well the class because all the models that conform to this Theory have in common let's say the way they interpret addition um and they all have in common that the values in the domain are some numbers right otherwise you couldn't really give interpretations so um a theory then gives you kind of a huge set of different models because the the all all you require from the models is that all these models uh if they belong to one Theory they must satisfy the aums of the theory and we will look at uh yeah some examples so for example equality um that's already a non-trivial theory how can this be equality is so easy right it means the thing on the left and right side is the same but uh it's not that easy um and and that's not that's not because of uh satisfiability module Theory this complexity is not related to the tools that we're going to use it's just that inherently mathematically to Define what does equality mean you need this stuff um or that's what let's say the world has agreed on this is what equality means so for example the world has agreed that equality means uh uh that we have reflexivity so that an element is equal to itself that's this reflexivity um if you find an element it must be or well actually all elements all elements they must be equal to themselves then uh we have symmetry so if x is equal to Y then y also needs to be equal to X there not a given right if x uh sorry if if equals is just some kind of predicate like hates then hates doesn't have to have symmetry right um nobody requires that but for equality we do require this so for equality we require that if x is equal to Y then Y is also equal to x no matter what X and Y are right for all possible things that X and Y could be then transitivity so if we have x equals Y and Y equals z then also X must be equal Z right so if the first is equal to the second and the second is actually the same as the third then the first and the third also must be the same otherwise there's something wrong with equality right um any property missing or is this all you expect to have from equality who was thinking that equality is even simpler than this well if we Define equality as some relation then we want all these things to hold and actually uh there's slightly more if we relate uh um yeah further uh for example uh functions then um we also want that if I have a function and I call this function on a set of variables and my variables my AIS are the same as the Y so basically I I feed the same function the same values um then I want the function to return the same uh result right so if I say x is uh one and I want to evaluate 1 plus well sorry I want to evaluate x + 1 then I get two right um and if I say Y is equal to one and I want to evaluate y + 1 I should also get two I shouldn't get a different value right so and that's exactly what it says here if if the X and the Y are the same then the function called on the X and the function called and the same function called on the Y Must also be the same um and that's then congruence and then finally we have uh another axium called equivalence so for all again variables X and Y if they are the same and I evaluate a predicate on them uh then this also has to get has to give the same Boolean value so this is now like the if and only if that's basically um if the same predicate is uh called on the same values because these variables evaluate to the same values then uh the predicates have to also give me the same uh yeah result again okay so that's equal now we have uh I think this now these five aums they they finally give us the theory of equality and now we can uh work with equality the way we used to work with it right uh sometimes you write things on the left sometimes you write them on the right and you're expecting that it's still the same right so same meaning so that's the Symmetry now yeah go ahead use your symmetry it's now fixed as aums and you can rely on it let's have a look at some examples so it's I mean all these rules they're not really anything um ah sorry that's piano arithmetic how come I think the example is missing um yeah let's skip this for now because I think this one yeah this is the next actually it's uh uh I'm missing the examples so let's um yeah there are no equality examples here um so yeah that was the theory of equality so this this is all stuff you you all knew in the back of your head in the back of your mind you all knew these right they're not new uh now uh something else piano arithmetic so that's uh some very uh simple form of arithmetic where you have the constants 01 you have plus and multiplication and equality um this is based on taking all the aums that we had before so we we take our equality now as a theory we say we're we're kind of taking all of these aums that we had before and we have additional aums so we have uh uh a zero kind of definition so um for all x x + one equals z is not possible so this basically means that you cannot get to Zero by using addition in this uh Theory here so there's basically uh you have zero and you have addition but you can never get back to uh Zero by adding one to anything because we don't have negative numbers here right so uh yeah this is the definition of zero then we have a definition of the successor um so x + 1 if that equals y + 1 uh then we have xal y and uh so basically the successor no matter what the uh value on the left is the successor always gives us the unique next thing it doesn't give us um if the variable is I don't know x equals 5 or xals 6 it never gives us the same value then uh if this gives the same value it means that the two variables were had the same value uh yeah then we have some further aums for doing induction we have uh that zero is basically the neutral element so if we have X +0 we end up with X um and we have well the successor of the plus that we can if we have X Plus and then the successor of something it's the same as doing the addition first and then taking the successor function so these are some uh yeah some rules that you might have had in some some early proofs in in in school we use that and we have like uh yeah multiplication with zero always is zero um and then of course we need to Define what uh what multiplication means and you can Define multiplication by saying well x * the successor of Y is x * y + x so yeah um and then you basically R use one from the the Y until you end up with zero and and this long addition there so multiplication is defined as well a bunch of additions but that's only um as an axium right this is only some law that our multiplication has to satisfy so how we actually do multiplication whether we actually do it with addition or not that doesn't matter it just has to satisfy this this law right so uh that's all and um yeah the so that's that's giving us some very simple stuff is this already enough for our cats and dogs and Mouse puzzle so we had uh well of course equality right uh then ah we had something like 100 we should buy 100 how do we do 100 in piano arithmetic we don't really have other numbers right we only have zero and one so basically this is this this really annoying arithmetic where you have to write the let's say two you have to write two as 1+ one you have to write three as 1 + 1 + 1 so this is like the successor function so 100 you would have to write as uh well 1 plus 1+ one and this thing uh well like 100 times um okay but then we can basically uh we have multiplication we have addition um the only thing we had was this like greater or equal right we said uh uh the um we had this kind of in equality so we we will probably have some additional theory of inequality but then we could represent with this arithmetic uh we didn't do any division right no I don't think so so yeah so with this thing we could already represent our deck our dogs cats and Mouse puzzle um that's great so we we managed the Agatha thing we managed the catto Mouse puzzle uh we had this one with the Emojis where we had like formulas over emojis this had division right so we we might have to have another theory for that um but you can imagine how this goes there are more theories uh and we're not going to go over all of them because there are tons of them and uh there are basically um yeah libraries where you can look at what theories exist uh there are many built-in theories in the tools that we will use um and everything should be fine to solve our puzzles but now it says here piano arithmetic is undecidable um what does that mean anybody got a clue is that good is that bad what does undecidable mean sorry cannot decide the outcome we cannot decide the outcome so here the uh kind of the problem would be um maybe given some uh formula find a model or or given some formula in the model is it uh so I think here the solution would be can we find a model for some formula and it's undecidable so there is no algorithm which can do it for all cases there are cases where an algorithm can do it otherwise we would be doomed right but there are some cases where an algorithm or any algorithm would fail to produce a uh solution so uh but now let's not yeah let's let's let's not skip ahead let's look at first some simple examples ah but this requires all the aums um sorry they all true ah some people already answered okay um so x + 1 = y + 1 implies X = Y um this was sorry which one successor yeah okay so that was directly an axum of course then trivially yes it's true um x + 1 = y implies uh Y is not zero that was the the zero thing and the equality with Y right so we have had to kind of mix um yeah then uh x + 1 * 0 = 0 that's here the time zero and our X was a bit more uh well this is for all X right so our X X plus one of course then it's also for X plus one okay um and the last one here that's also the uh yeah extraction of the times but we have two times the successor so we basically have to apply this axium twice if we want to solve it like that okay yeah so all of them were true exactly good um and then uh of course now we we are interested in um satisfiability and now we're interested in satisfiability given a theory right so we have this theory of piano arithmetic we have the theory of equality so now we should relate this to satisfiability so the way we can relate this is we say some formula is T satisfiable in t satisfiable in this Theory T if there is a model for the theory so the model must respect all the axioms we gave in the theory um where our formula evaluates to true so um now if we want to say that this holds in this uh Theory T we could write the T as a subscript of these models um because there might be different models and not all the models might um satisfy the theory axioms and of course if we have a specific theory in mind like the equality we we would always be interested only in models that actually satisfy the equality as we know it if there's some model and it defines it redefines equality then we're not really interested in this right so we usually interested in some t satisfiability for some chosen theories that we are using and we will see that in all those cases that uh we're dealing with uh the theories they can be automatically chosen so basically uh the tool that we will use it will choose the right theories for us automatically because there's not really a clash on the theories that we use so if there's something about arithmetic it will choose the right arithmetic for us and uh we don't need to even care about which Theory to say we want to use it will use the appropriate ones for us but there are some where we might want to to import additional theories but uh yeah not in this lecture okay so um and then of course there's also validity with respect to some Theory so we can say that some formula is T valid in some Theory T if um yeah for all the assignments to the variables to the free variables of the formula uh this formula is in the theory um so yeah it evaluates the true for every model of the theory so no matter what assignment our model gives to the uh yeah to the three variables it would evaluate to true so um and then that would be T validity and we could write it yeah without this model because it's basically for any model um conforming to the theory okay um now let's have a look at some first logic with theory of uh equality oh I have to look the other [Music] one so now if we want to select all the equalities determined by the theory of equality for these variables XY functions FG and predicates p and Q maybe that's the question that should have been there earlier right I think that's just something wrong with the order so I'll go back to the yeah probably need these aims here right uh okay okay so let's have a look the first one yeah that's determined by the theory of equality and that's the reflexivity right so reflexivity gives oh gives the answer to the first one what about the second one ah it's not determined by the theory of equality uh why not well we see here the parameters there are here's an X and there's a y and we don't have any further information right we don't know how X and Y relate so the theory of equality doesn't determine anything here we don't have an axium that tells us you can combine these aums and and you know it what about this one F of XX equals F of XX and uh which one which exm tells us the congruent because that congruent says if we call it on the uh on variables which are have the same value uh well here we even have the same name right but still it's the the congruence axum which tells us yeah this one is uh ah sorry yeah this one is is true what about this one FSE false because the congruence requires that it's the same F right it's the same function so we don't know how G and F are related so we don't know there might be models where this is true but then it's not determined by the theory then it would be determined by the model um okay then um these ones here that a predicate of x equals the predicate of Y for xal y that's basically the yeah equivalence relation here or equivalence uh axum here yeah for uh because we have this xals Y and then yeah they are equivalent okay good um so now um what about satisfiable formulas in first logic with a theory of equality so what does this now mean this means that if we have some model uh this model has to conform to the all the axioms of equality so it can't really break them um otherwise it might be too easy right otherwise if you say uh your uh equality could be arbitrarily defined then you can maybe always find a model that satisfies them but now this model has to uh give us a real equality as we know it right so okay so what about the first one x equals true uh the model can simply uh give the Val a value uh that it like it it can the constant true can be mapped to the value true in the domain and X can be interpreted X is a variable so X can be also interpreted as the value true right so that's clearly something satisfiable we can give easily some model that satisfies that right um what about the second one for all X there exists a y such that xals y so now we have this uh yeah what do we have do we have any uh thing that we can use any axium that we need to rely on well I mean reflexivity might be a good axum to rely on uh that if we put the same element on the left and on the right it's giving us the same thing now the question is is the same element can the same element be picked so we have to the fall all says it picks some value for uh well the for all has to go over all values of the domain right so if these are integers um let's say it starts with I don't know one um then x equals 1 okay now exist does there exist a y so some value from our domain that makes x equal y yeah so if we we can assign also one here right um because we just have to find a single one so then it's one equal 1 fine now the for all says but you have to check all values so let's say xal 2 uh can we find a value that is equal to two yes of course two is equal to two so yeah uh this thing works fine so this one should also be true like yeah the majority said okay then there exists an x uh such that for all Y X is not y why can we not find this why would that be true H sorry why would that be false yeah ah but uh here these things actually say we have to do it for all values right the for all quantifier X and Y are not free variables so we can't really arbitrarily choose they have to go through all values of the domain uh so and and no matter what domain we we choose with uh equality this means that um let's say we pick one value and then we have to pick each existing each each possible value again so we have to pick also the value that we previously picked right because we have to pick all the values in the domain so this means that we will if we pick tier one we have to pick one here at some point if we picked here five we have to pick five here at some point and then then there's no way that five does not equal five because of the um yeah reflexivity okay so the last one is not uh satisfiable um of course if we didn't have the quantifiers then it was easily satisfiable because then uh the model could just give some assignment of X and some assignment of Y so that they're not the same right so then we could assign X1 and y5 okay yeah um yeah so much about uh equality uh we had arithmetic already we had satisfiability validity and um yeah next session we will continue with this issue of undecidability what it actually means but uh yeah this will be next week and then uh yeah we will we will get there and see what the limitations are um yeah so see you next week