6.13 - Finite relational logic - Relational logic - [introduction to logic] by michael genesereth

Finite relational logic or FRL is that subset of relational logic in which the Herbrand base is finite. In order to guarantee a finite Herbrand base, we must restrict ourselves to signatures or vocabularies in which there are, at most, finitely many object constants and no function constants at all. One interesting feature of FRL, is that it's expressively equivalent to propositional logic, which will call PL from here on out. For any FRL language, we can produce a pairing between the ground relational sentences in that language, and the proposition constants in a propositional logic language. Given this correspondence, for any set of arbitrary sentences in our FRL language, There's a corresponding set of sentences in the language of PL, Such that any FRL truth assignment that satisfies our FRL sentences agrees with the corresponding PL truth assignment applied to the PL sentences. The procedure for transforming our FRL sentences to PL has a few steps, but each step is easy. First, we convert to prenex form. And then we ground the result. And finally, we rewrite into propositional logic. Let's take a look at each of these steps in turn. A sentence is defined to be in pre, prenex form, if and only, if it's closed, and all the quantifiers are on the outside of all logical operators. For example, the first sentence here is in prenex form. The two sentences at the bottom are not in prenex form. The first fails because the quantifiers are inside illogical operators. And the second one fails because the sentence contains a free occurrence of y. Converting a set of sentences from FRL to a logically equivalent set of sentences in prenex form is really easy. First, in case there are any conflicts, we rename variables in different quantified sentences to eliminate those conflicts. An example shown here we rename the variable y in the second disjunct. In the second step, we apply quantifier distribution rules to move quantifiers outside of logical operators. Here, we have two cases of that. And finally, we universally quantify any free variables in our sentences. In this case, the variable x is free in the sentence, and so we add either as a quantifier for x. Once we have a set of sentences in prenex form, we can compute its grounding. The procedure is described here. We start with our initial set of sentences and we incrementally build up our grounding. The initial set is called delta. The grounding is going to be called gamma. On each step, we process a sentence in delta using these rules. The procedure terminates when delta becomes empty. The set gamma at that point is then the grounding of the input. The first rule covers the case when the sentence being processed is ground. In this case, we remove the sentence from delta and simply add it to gamma. If the sentence is of the form, for all nu, phi of nu, some variable nu, some formula phi, we remove the sentence from delta and add in an instance of the target of the sentence, in other words, phi, for each object constant in our language. If the sentence is in the form that there exists a nu, such that the phi of nu is true, true is included, if we removed the sentence from delta and add in a disjunction in which each disjunct is an instance of the target for a different object constant in the language. Let's look at an example of this. Suppose we have a language with just two object constants, A and b. And suppose we have the set of sentences shown here. We have one ground sentence, one universally quantified sentence, and one existentially quantified sentence. All of them are in prenex form. On the first step, we remove the ground sentence, p of a from delta and we add it to gamma. On the second step, we remove the universally quantified sentence from delta and add instances back into delta, Instances of the target of that sentence. In this case, we have p of a implies q of a, And p of b implies q of b. Note that we don't add the, these instances directly to gamma just yet because, in general, they might contain nested quantifiers but rather, we use the first rule to do that, to move them down. However, in the next two steps, we do to that because these senses are ground. So move p of a implies q of a down then, we move p of b implies q of b down. Despite, we have adjusted the existential sentence to process and we remove that from delta and replace with disjunction of the target with one disjunction for each consonant in our language, q of a or q of b. Finally, since this is a ground sentence, we remove it, we move it to gamma as well and we're done. Okay, once we have a grounding gamma, we replace each ground relational sentence in gamma by a proposition constant. Resulting sentences are then all in propositional logic. And the set of it's equivalant to the sentences of gamma and that any FRL truth asignment that satifies our FRL sentences agrees with the corresponding propostional logic truth assignment applied to those propositional logic sentences. So, for example here, let's represent the FRL sentence p of a, A, a proposition p pa, let's represent p of a sorry, a of a with qa. Let's represent q of b with qb, And so forth. With this correspondence, we can represent the FRL sentences, shown at the top here, with the propositional logic sentences shown at the bottom. Now, the import of all of this is decidability. Since the question of unsatisfiabilty for propositional logic is decidable then, because of this equivalence, we know that the question of unsatisfiabilty for FRL is also decidable. And since logical entailment and unsatisfiabilty are correlated, we know the same is true for logical entailment. Namely, it is decidable as well. And there is one more consequence of this correspondence between the two languages. Frl like PL is compact, in other words, every unsatisfied sentences contains a finite subset that is unsatisfiable. This is important because it ensures us that we can demonstrate unsatisfiability with just the finite set of sentences. And also as we'll see in the next lessons, logical entailment can be demonstrated with finite proofs.