2.9. Normal Form Implementations 35
2.9 Now that we have algorithms for converting formulas into clause and
dual clause forms, we want to embody these algorithms in programs.
We have chosen the language Prolog for this job because it lets us get Implementa- to the heart of the matter with a minimum of preliminary detail. We do
Copyright By PowCoder代写 加微信 powcoder
Normal Form
not discuss the general ideas of programming in Prolog; several readily available books do this. A recommended standard here is provided by Clocksin and Mellish [10]; another more advanced work is Sterling and Shapiro [51].
Prolog allows one to define ‘operators.’ Essentially, this is a matter of convenient syntax. For example, we can specify that the name and will always be used as an infix binary connective, and hence p and q will be meaningful. Prolog also allows one to specify an order of precedence and whether infix operators will be left or right associative. In the implemen- tation that follows we specify neg to be a prefix operator, which we use to stand for –, (we do not use not, because this already has a meaning in most Prologs). For the Primary Connectives, we use and for !\, or for V, imp for ~, revimp for C, uparrow for i, downarrow for 1, notimp for 1;, and notrevimp for rt. We assume all occurrences of == and t= have been translated away. neg is defined to have a precedence of 140. The Primary Connectives are all defined to be infix, right associative, and are given precedences of 160. All this is done at the beginning of the program, using the op predicate. The precedence numbers selected may need to be changed for different Prolog implementations, and the syntax appropriate for the op predicate varies somewhat too. Apart from this, the program should work as written in any ‘Edinburgh syntax’ Prolog.
Before giving the Prolog program, a word about its abstract structure may help. Suppose we call a directed graph well-founded if, for each node a, every path starting at a is finite. Starting at any node in such a graph, at a, say, there is at least one maximal path, which begins at a and ends at a node with only incoming edges, and we can find such a path by simply following edges until we can’t do so any further. Now, suppose we have clauses for a Prolog predicate that generates the edges of a well-founded, directed graph; say the predicate edge (X, Y) is true exactly when X and Y are nodes and there is an edge from X to Y. Then there is a simple, and standard, way of writing a graph search program to find maximal paths. We just add the following clauses:
path(X, Y) :- edge(X, Z), path(Z, y). path(X, X).
Now consider the following graph: The nodes are disjunctions of conjunc- tions. There is an edge from node One to node Two if the application of a single Dual Clause Set Reduction Rule will turn One into Two. (This corresponds to a single pass through the while loop of the Dual Clause
Fitting, Melvin, and . First-Order Logic and Automated Theorem Proving, edited by . Schneider, Springer New York, 1995. ProQuest Ebook Central, http://ebookcentral.proquest.com/lib/warw/detail.action?docID=3077179.
Created from warw on 2022-04-26 11:57:08.
Copyright © 1995. Springer New York. All rights reserved.
36 2. Propositional Logic
Form Algorithm.) The Dual Clause Form Algorithm is correct, and this amounts to saying that if we start at a node and follow edges until we reach a node with only incoming edges, that node will be a dual clause form of the node at which we started. Also, the Dual Clause Form Al- gorithm strongly terminates, and this amounts to saying that the graph we have created is well-founded.
Now, the Prolog program is easily described. The singlestep predicate generates edges in the graph just described. We want to find maximal paths. The predicate that corresponds to path is now called expand, for obvious reasons. Finally, there is a ‘driver’ predicate, dualclauseform, that simply takes an ordinary formula X, turns it into the equivalent of [(X)], and calls on the expand predicate. For convenience both general- ized conjunctions and generalized disjunctions are represented as lists; context can easily determine which is meant. So, finally, to use the pro- gram for converting a formula x to dual clause form, enter the query dualclausef orm (x, V), where V is a Prolog variable. Prolog will return a value for V that is a list of the dual clauses making up the dual clause form.
1* Dual Clause Form Program
Propositional operators are: neg, and, or, imp, revimp,
uparrow, downarrow, notimp and notrevimp.
?-op(140, fy, neg).
?-op(160, xfy, [and, or, imp, revimp, uparrow, downarrow,
not imp , notrevimp]).
1* member(Item, List) :- Item occurs in List.
member(X, [X -]) .
member (X, [_ T ail]) :- member (X , T ail).
1* remove (Item, L ist, Newlist) :-
Newlist is the result of removing all occurrences of Item from List.
remove(X, [], []).
remove(X, [X I T ail], Newtail)
remove (X, T ail, Newtail).
remove (X, [Head I T ail], [Head I Newtail])
Fitting, Melvin, and . First-Order Logic and Automated Theorem Proving, edited by . Schneider, Springer New York, 1995. ProQuest Ebook Central, http://ebookcentral.proquest.com/lib/warw/detail.action?docID=3077179.
Created from warw on 2022-04-26 11:57:08.
Copyright © 1995. Springer New York. All rights reserved.
2.9. Normal Form Implementations 37
remove(X, T ail, Newtail).
1* conjunctive (X) :- X is an alpha formula.
conjunctive(_ and _). conjunctive(neg(_ or _)). conjunctive(neg(_ imp _)). conjunctive(neg(_ revimp _)). conjunctive(neg(_ uparrow _)). conjunctive(_ downarrow _). conjunctive(_ notimp _). conjunctive(_ notrevimp _).
1* disjunctive (X) :- X is a beta formula. *1
disjunctive(neg(_ and _)). disjunctive(_ or _). disjunctive(_ imp _). disjunctive(_ revimp _). disjunctive(_ uparrow _). disjunctive(neg(_ downarrow _)). disjunctive(neg(_ notimp _)). disjunctive(neg(_ notrevimp _)).
1* unary(X) :- X is a double negation, or a negated constant.
unary(neg neg _). unary(neg true). unary(neg false).
1* components (X, Y, Z) Y and Z are the components of the formula X, as defined in the alpha and beta table.
components(X and Y, X, Y). components(neg(X and Y), neg X, neg Y). components(X or Y, X, Y). components(neg(X or Y), neg X, neg Y). components(X imp Y, neg X, Y). components(neg(X imp Y), X, neg Y).
Fitting, Melvin, and . First-Order Logic and Automated Theorem Proving, edited by . Schneider, Springer New York, 1995. ProQuest Ebook Central, http://ebookcentral.proquest.com/lib/warw/detail.action?docID=3077179.
Created from warw on 2022-04-26 11:57:08.
Copyright © 1995. Springer New York. All rights reserved.
38 2. Propositional Logic
components(X revimp Y, X, neg Y). components(neg(X revimp Y), neg X, y). components(X uparrow Y, neg X, neg y ) . components(neg(X uparrow Y), X, y). components(X downarrow Y, neg X, neg Y). components(neg(X downarrow Y), X, Y). components(X notimp Y, X, neg Y). components(neg(X notimp Y), neg X, Y). components(X notrevimp Y, neg X, Y). components(neg(X notrevimp Y), X, neg Y).
1* component(X, Y) Y is the component of the unary formula X.
component(neg neg X, X). component(neg true, false). component(neg false, true).
1* singlestep(Old, New) :- New is the result of applying a single step of the expansion process to Old, which is a generalized disjunction of generalized conjunctions.
singlestep([Conjunction I Rest], New)
member (Formula, Conjunction),
unary (Formula) ,
component (Formula, Newformula),
remove (Formula, Conjunction, Temporary), Newconjunction = [Newformula I Temporary], New = [Newconjunction I Rest].
singlestep([Conjunction Rest], New)
member (Alpha , Conjunction),
conjunctive (Alpha) ,
components (Alpha, Alphaone, Alphatwo), remove (Alpha, Conjunction, Temporary), Newcon = [Alphaone, Alphatwo I Temporary], New = [Newcon I Rest].
singlestep([Conjunction I Rest], New) member(Beta, Conjunction), disjunctive (Beta) ,
components (Beta, Betaone, Betatwo),
Fitting, Melvin, and . First-Order Logic and Automated Theorem Proving, edited by . Schneider, Springer New York, 1995. ProQuest Ebook Central, http://ebookcentral.proquest.com/lib/warw/detail.action?docID=3077179.
Created from warw on 2022-04-26 11:57:08.
Copyright © 1995. Springer New York. All rights reserved.
2.9.1p . Write a Prolog program for converting a propositional formula into clause form.
2.9.2P . Write a Prolog program implementing the algorithm for con- verting a propositional formula into negation normal form that was pre- sented at the end of Section 2.5.
2.9.3P . Write a Prolog program for translating away occurrences of == and ¢.
2.9.4P • Write a Prolog program implementing the degree function defined in Exercise 2.2.2 and another implementing the rank function defined in Definition 2.6.5.
remove(Beta, Conjunction, Temporary), Newconone = [Betaone I Temporary], Newcontwo = [Betatwo I Temporary], New = [Newconone, Newcontwo I Rest].
singlestep([ConjunctionIRest], [ConjunctionINewrest]) singlestep(Rest, Newrest).
1* expand(Old, New) :- New is the result of applying singlestep as many times as possible, starting with Old.
expand(Dis, Newdis) :- singlestep(Dis, Temp), expand (Temp , Newdis).
expand(Dis, Dis).
1* dualclauseform(X, Y)
dualclauseform(X, Y)
Y is the dual clause form of X. expand([[X]], Y).
Fitting, Melvin, and . First-Order Logic and Automated Theorem Proving, edited by . Schneider, Springer New York, 1995. ProQuest Ebook Central, http://ebookcentral.proquest.com/lib/warw/detail.action?docID=3077179.
Created from warw on 2022-04-26 11:57:08.
Exercises 39
Copyright © 1995. Springer New York. All rights reserved.
3___________________________________
Semantic Tableaux and Resolution
3.1 We will present several proof procedures for propositional logic in this
chapter and the next. Two of them are especially suitable for automa-
tion: resolution [42] and semantic tableaux [48]. Of these, resolution is Semantic closely connected with conjunctive normal or clause forms, while the se-
Propositional
mantic tableaux system is similarly connected with disjunctive normal or dual clause forms. We discuss semantic tableaux rules in this section and resolution in Section 3.3. We begin with a general description that is suited to either hand or machine implementation and give a Prolog implementation in Section 3.2.
Both resolution and tableaux are refutation systems. To prove a formula X, we begin with oX and produce a contradiction. The procedure for doing this involves expanding oX so that inessential details of its logical structure are cleared away. In tableaux proofs, such an expansion takes the form of a tree, where nodes are labeled with formulas. The idea is that each branch should be thought of as representing the conjunction of the formulas appearing on it and the tree itself as representing the disjunction of its branches.
To begin, we restate the Dual Clause Set Reduction Rules from Sec- tion 2.8, but now we call them Tableau Expansion Rules. They are given in Table 3.1
Next we say something about how the rules in Table 3.1 are intended to be applied. Basically, they allow us to turn a tree with formulas as node labels into another such tree. Suppose we have a finite tree T with
Fitting, Melvin, and . First-Order Logic and Automated Theorem Proving, edited by . Schneider, Springer New York, 1995. ProQuest Ebook Central, http://ebookcentral.proquest.com/lib/warw/detail.action?docID=3077179.
Created from warw on 2022-04-26 11:57:08.
Copyright © 1995. Springer New York. All rights reserved.
3. Semantic T ableaux and Resolution
Definition 3.1.1
TABLE 3.1. Tableau Expansion Rules
nodes labeled by propositional formulas. Select a branch eand a non- literal formula occurrence X on e. If X is ” Z , lengthen eby adding a node labeled Z to its end. Similarly, if X is ,T , add ~, and if X is ,~, add T. If X is a, add a node to the end of elabeled a1 and another node after that labeled a2. Finally, if X is /3, add left and right children to the final node of e, and label one /31 and the other /32′ Call the resulting tree T*. We say T* results from T by the application of a Tableau Expansion Rule. If it is necessary to be more specific, we may say T* results from the application of the a-rule, or whichever, to formula occurrence X on branch e.
Now we define the notion of a tableau. Our definition is a little more general than we need at the moment since we allow finite sets of formulas at the start. The added generality will be of use when we come to prove completeness. The definition is a recursive one.
Let {All”” An} be a finite set of propositional formulas.
1. The following one-branch tree is a tableau for {A 1 , • • . , An}:
2. If T is a tableau for {A1, … , An} and T* results from T by the application of a Tableau Expansion Rule, then T* is a tableau for {A1, … ,An}.
Figure 3.1 shows a tableau for {P 1(Q V R), ,(Q 1\ ‘R)}. The numbers are not an official part of the tableau but have been added to make talking about it easier. In this tree, 1 and 2 make up the set the tableau is for; 3 and 4 are from 2 by the /3-rule; 5 is from 4 by the ” rule; 6 and 7 are from 1 by the a-rule; 8 and 9 are from 7 by the a-rule. Notice that we never applied the a rule to 1 on the right-hand branch. Also, we chose to apply a rule to 2 before we did to 1.
Fitting, Melvin, and . First-Order Logic and Automated Theorem Proving, edited by . Schneider, Springer New York, 1995. ProQuest Ebook Central, http://ebookcentral.proquest.com/lib/warw/detail.action?docID=3077179.
Created from warw on 2022-04-26 11:57:08.
Copyright © 1995. Springer New York. All rights reserved.
Definition 3.1.2
Definition 3.1.3
3.1. Propositional Semantic Tableaux 43
1. p HQvR) 2A. ….,(Q /\ ….,R)
3. ….,Q 4. ….,….,R 6. ….,p 5. R
7. ….,(Q V R) 8. ….,Q
FIGURE 3.1. Tableau for {P ! (Q VR), ….,(Q/\ ….,R)}
A branch () of a tableau is called closed if both X and ….,X occur on () for some propositional formula X, or if …L occurs on (). If A and ….,A occur on () where A is atomic, or if …L occurs, () is said to be atomically closed. A tableau is (atomically) closed if every branch is (atomically) closed.
As we remarked earlier, both tableau and resolution-style proofs are refutation arguments. That is, a proof of X amounts to a refutation of ….,X.
A tableau proof of X is a closed tableau for {….,X}. X is a theorem of the tableau system if X has a tableau proof. We will write I-pt X to indicate that X has a propositional tableau proof.
Figure 3.2 shows a tableau proof (with numbers added for reference) of [(p:J (Q :J R)) :J «P VS) :J «Q :J R) VS))]. In it, 1 is the negation ofthe formula to be proved; 2 and 3 are from 1 by Q; 4 and 5 are from 3 by Q; 6 and 7 are from 5 by Q; 8 and 9 are from 2 by /3. 10 and 11 are from 4 by /3. Reading from left to right, the branches are closed because of 8 and 10, 7 and 11, and 6 and 9. Notice that on one of the branches closure was on a non-atomic formula.
Of course, we must establish that the tableau procedure does what we want. To be precise, we must show soundness: anything provable is a tautology (Section 3.4). And we must show completeness: all tautologies have proofs (Section 3.7). Indeed, we will show a particularly strong ver- sion that says, as long as we eventually apply every Tableau Expansion Rule once to every non-literal formula occurrence on every branch, we
Fitting, Melvin, and . First-Order Logic and Automated Theorem Proving, edited by . Schneider, Springer New York, 1995. ProQuest Ebook Central, http://ebookcentral.proquest.com/lib/warw/detail.action?docID=3077179.
Created from warw on 2022-04-26 11:57:08.
Copyright © 1995. Springer New York. All rights reserved.
44 3. Semantic Tableaux and Resolution
1. –.[(P~(Q~R))~((PVS)~((Q~R)VS))] 2. P ~ (Q ~ R)
3. –.((PVS)~((Q~R)VS))
5. –.((Q~R)VS) 6. –.(Q ~ R) 7.A–.S
~.–.P 9.Q~R 10. P 11. S
FIGURE 3.2. Proof of [(P ~ (Q ~ R)) ~ ((P V S) ~ ((Q ~ R) V S))] will find a proof if one exists. We will also show that testing for closure
can be restricted to the level of literals without affecting completeness.
Tableau proofs can be very much shorter than truth table verifications. As a trivial example, if X is a propositional formula with n propositional variables, a truth table for XV–.X will have 2n lines, but a closed tableau begins with –.(X V –.X), proceeds with the a rule to add –.X and –.–.X, and is closed at this point (though it is not atomically closed). Further, the tableau method extends easily to handle quantifiers, while the truth table method does not.
The tableau rules are non-deterministic-they say what we may do, not what we must do. They allow us to choose which formula to work with next, on which branches. They allow us to skip formulas or use them more than once. And they allow us to close branches at the atomic level or at a more complex level if we can. People generally find this freedom useful, and often judicious choices of rule applications can pro- duce shorter proofs than might be expected. On the other hand, when it comes to incorporating the tableau system in a deterministic computer program, some standardized order of rule applications must be imposed, and various limitations on the basic tableau freedom will be necessary. One limitation turns out to be very fundamental, and we discuss it now. As we remarked, in constructing tableaux we are allowed to use formulas
over and over. For instance, if a occurs on a branch, we can add a l and a2, and later we can add al and a2 again, since a is still present. For certain non-classical logics, this ability to reuse formulas is essential (see
Fitting, Melvin, and . First-Order Logic and Automated Theorem Proving, edited by . Schneider, Springer New York, 1995. ProQuest Ebook Central, http://ebookcentral.proquest.com/lib/warw/detail.action?docID=3077179.
Created from warw on 2022-04-26 11:57:08.
Copyright © 1995. Springer New York. All rights reserved.
Definition 3.1.4
3.1. Propositional Semantic Tableaux 45
Fitting [16]). But if we are allowed to reuse formulas, how do we know when we should give up on a proof attempt? After all, there will always be something we can try; if it didn’t work before, maybe it will now. Fortunately, for classical propositional logic, it is never necessary to use a formula more than once on any branch. This makes the task of imple- menting tableaux easier. On the other hand, it makes the proof of tableau completeness somewhat more work. If we allow the reuse of formulas, completeness of the tableau system can easily be proved by a general method, based on the Model Existence Theorem from Section 3.6, and this same method allows us to prove the completeness of many other types of proof procedures. If we impose a no-reuse restriction, the easy general methods fail us, and we must introduce other techniques. Since the restriction is so important, we introduce some special terminology for it.
A tableau is strict if in its construction no formula has had a Tableau Expansion Rule applied to it twice on the same branch.
In constructing strict tableaux by hand, we might keep track of which formulas have had rules applied to them by simply checking them off as they are used. But a formula occurrence may be common to several branches, and we may have applied a rule to it on only one of them. An easy way of dealing with this is to check the occurrence off but add fresh occurrences at the ends of those branches where we have not used it.
A strictness restriction is of more importance for machine implementa- tion. In our implementation we will represent a tableau as a list of its branches, and a branch as a list of its formulas. (This is the same data structure we used for the Dual Clause Form Algo
程序代写 CS代考 加微信: powcoder QQ: 1823890830 Email: powcoder@163.com