Transcript Using Existential Graphs for Automated Theorem Proving

Using Existential Graphs for
Automated Theorem Proving
Bram van Heuveln
March 13, 2002
Overview
• Automated Theorem Proving
– What is it?
– ATP procedures
• Existential Graphs
– Quick Overview
– Using EG for ATP
Automated Theorem Proving
• In ATP, one tries to come up with procedures that
check whether some statement  (the conclusion,
or theorem) logically follows from (is logically
entailed by; is a logical consequence of) a set of
statements  = {1 ,  , n} (the premises, or
axioms).
• In this definition, ‘logically’ means ‘according to
some system of logic’. This talk, we will restrict
ourselves to the system of truth-functional logic. I
will assume the audience to be familiar with the
formal syntax and formal semantics of truthfunctional logic.
Decision Procedures
• A procedure P that checks for logical entailment is
called a decision procedure if and only if for any
statement  and any set of statements :
– (P is a positive test) P declares that  is logically
entailed by  if and only if  is indeed logically
entailed by , and
– (P is a negative test) P declares that  is not logically
entailed by  if and only if  is indeed not logically
entailed by 
(these two properties are crucially different, since not
declaring that something is the case is not the same as
declaring that something is not the case. E.g. consider P
going into an infinite loop)
Logical Entailment and Logical
Consistency
• Logical Entailment:
– A statement  is a logical consequence of a set of statements  =
{1, …, n} if and only if it is impossible for  to be false while
each i is true. We write this as  |= 
• Logical Consistency:
– A set of statements  = {1, …, n} is logically consistent if and
only if it is possible for each i to be true.
• So, a statement  is logically entailed by a set of
statements {1, …, n} if and only if the set {1, …, n,
} is logically inconsistent.
• Therefore, a decision procedure for logical entailment can
be used as a decision procedure for logical consistency,
and vice versa. We will see both main types of decision
procedures in this talk.
Procedures for checking logical
entailment or logical consistency
•
•
•
•
•
•
•
Derivations
Truth Tables
Short Truth Tables
Truth Trees
Resolution
Davis-Putnam
Non-Clausal Davis-Putnam
Running Problems
K  (L  M)
M  L
U  (V  W)
UW
(P  Q)
(Q  R)
M
V
PR
Is {(X  Y), (X  Y), (X  Y), (X  Y)} consistent?
A  (B  C)
(A  B)  (D  E)
E
A
CD
Derivations
• Systems of derivation define a finite number of
rules of inference that allow one to infer (derive) a
statement from other statements.
• A formal proof is a sequence of statements, where
each statement is either an assumption, or is
derived from any of the previous statements using
some rule of inference.
• If there is a formal proof with 1, …, n as initial
assumptions, and with  as the last statement, then
we write {1, …, n } |- 
Derivation Example
1.
2.
3.
4.
5.
6.
7.
8.
9.
10.
11.
A  (B  C)
(A  B)  (D  E)
E
A
BC
B
C
AB
DE
D
CD
Assumption
Assumption
Assumption
Assumption
DS 1,4
Simp 5
Simp 5
Add 6
MP 2,8
DS 3,9
Conj 7,10
The Good, the Bad, and the Ugly
• The good news is that there exist systems of
derivation (e.g. Fitch) for which it holds that for
any statement  and any set of statements :
– (Soundness) If  |-  then  |= , and
– (Completeness) If  |=  then  |- 
• The bad news is that the systems do not tell us
how to construct a formal proof.
• The ugly news is that the systems are unable to tell
us that  is not logically entailed by .
– With some effort, a decision procedure can be based on
derivational systems, but it is going to be inefficient.
Truth Tables
• Truth tables systematically exhaust all
possible truth-value assignments.
• The good news is that this will provide us
with a decision procedure.
• The bad news is that it is a very inefficient
procedure.
Truth Table Example
U
T
T
T
T
F
F
F
F
V
T
T
F
F
T
T
F
F
W
T
F
T
F
T
F
T
F
U  (V  W)
T
F
T
T
T
T
T
T
UW
T
F
T
F
F
T
F
T
V
F
F
T
T
F
F
T
T
A More Focused Search
K  (L  M)
M  L
M
• We are interested in whether all premises can be
true and the conclusion false:
– In order for the conclusion to be false, M must be false.
– In order for the second premise to be true while M is
false, L must be false.
– In order for the first premise to be true while L and M
are both false, K must be false.
The Short Truth Table Method
• The Short Truth Table Method assigns truth values
to the involved complex statements, and sees if
that can be made to work out:
K  (L  M)
F T F FF
ML
F TTF
/
M
F
works out  invalid
A  (B  C) (A  B)  (D  E) E A
F T T T T F ? T T F F F TF TF
does not work out  valid
/ C  D
T FF
Drawback of the Short Truth
Table Method
• A drawback of the short truth table method is that
you are not always forced to assign any further
truth values:
U  (V  W)
T T
UW
T
V
FT
• At this point, you can choose to assign certain
truth values, but if your choice does not lead to the
kind of row you are looking for, then you need to
try a different option, and the short truth table
method has no tools to do go through all of your
options in a systematic way.
Truth Trees
• The obvious solution to the drawback of the short
truth table method is to incorporate tools to
systematically keep track of multiple options.
• One method that does so is the truth tree method:
– The truth tree method tries to systematically derive a
contradiction from the assumption that certain
statements are all true.
– Like the short table method, it infers which other
statements are forced to be true under this assumption.
– When nothing is forced, then the tree branches into the
possible options.
Truth Tree Example
U  (V  W)
UW
V
V
U
U
W

VW
W
U V
W 

U
U
W
W
Decomposition Rules for Truth
Trees
P 
P
PQ 
P
Q
PQ 
PQ 
P
Q
P
(PQ) 
P
Q
Q
PQ 
P
Q
P
Q
(PQ) 
P
Q
(PQ) 
P
Q
(PQ) 
P
Q
P
Q
Rules of KE Calculus
P
P
DN
PQ
P
Q
(P  Q)
P
Q
Alpha


Branch
PQ
P
Q
PQ
P
Q
PQ
P
Q
(P  Q)
P
(P  Q)
P
PQ
Q
P
PQ
P
Q
(P  Q)
P
Q
Q
Beta
(P  Q)
P
Q
Eta
Q
Truth Trees as Decision
Procedures
• The truth tree method can easily be made
into a decision procedure.
• Efficiency can be increased by strategically
choosing sentences to be decomposed.
Resolution
• Resolution is, like the tree method, a method to check for
the logical consistency of a set of statements.
• Resolution requires all sentences to be put into CNF.
• A set of sentences in CNF is made into a clause set: a set
of clauses, where a clause is a set of literals.
• Clauses are resolved using the resolution rule, and the
resulting clause (the resolvent) is added to the clause set:
L  C1
L’  C2
CNEW = C1/L  C2/L’
Putting into CNF
(P  Q)
 (Equiv)
((P  Q)  (Q  P))  (Impl)
((P  Q)  (Q  P))
(P  Q)  (Q  P)
(P  Q)  (Q  P)
 (DeM)
 (DeM, DN)
 (Dist)
((P  Q)  Q)  ((P  Q)  P)
 (Dist)
(P  Q)  (Q  Q)  (P  P)  (Q  P)
Resolution Graph
(P  Q)

(P  Q)  (P  Q)

{P, Q} {P, Q}
(Q  R)
(P  R)


(Q  R)  (Q  R) (P  R)  (P  R)


{Q, R} {Q, R} {P, R}
{P, R}
{P, Q}
{P, R}
{P}
{P}
{}
Soundness and Completeness of
Resolution
• A clause is satisfied by a truth-value assignment if and
only if that assignment makes at least one literal in that
clause true.
• A clause set is satisfiable if and only if there is a truthvalue assignment that satisfies all clauses in that clause set.
• A set of sentences is inconsistent if and only if the
corresponding clause set is unsatisfiable.
• It can be shown that a clause set is unsatisfiable if and only
if the empty clause (which is a generalized disjunction of 0
disjuncts, which is a contradiction) can be resolved from
that clause set.
Resolutions as Derivations
A  (B  C)  (A  B)  (A  C) 
(A  B)  (D  E)

(A  D  E)  (B  D  E) 

E 
A 
(C  D)  C  D 
(A  B)  (D  E)  (A  B)  (D  E)
1. {A, B}
2. {A, C}
3. {A, D, E}
4. {B, D, E}
5. {E}
6. {A}
7. {C, D}
1,6
8. {B}
2,6
9. {C}
4,8
10. {D, E}
5,10
11. {D}
7,9
12. {D}
11,12
13. {}
Resolutions as Decision
Procedures
• Resolution can be made into a decision
procedure by systematically exhausting all
possible resolvents (of which there are
finitely many).
• This will not be very efficient unless we add
some resolution strategies.
Resolution Strategies
• Clause Elimination Strategies
– Tautology Elimination
– Subsumption Elimination
– Pure Literal Elimination
• Resolving Strategies
–
–
–
–
Unit Preference Resolution
Linear Resolution
Ordered Resolution
Etc.
Tautology Elimination
• A tautologous clause is a clause that contains an
atomic statement as well as the negation of that
atomic statement.
• Obviously, for any tautologous clause C, any
truth-value assignment is going to satisfy C.
• Hence, with S any clause set, and with S’ the
clause set S with all tautologous clauses removed:
S is satisfiable if and only if S’ is satisfiable.
Subsumption Elimination
• A clause C1 subsumes a clause C2 if and only if
every literal contained in C1 is contained in C1, i.e.
C1  C2.
• Obviously, if C1 subsumes C2 , then any truthvalue assignment that satisfies C1 will satisfy C2.
• Hence, with S any clause set, and S’ the clause set
S with all subsumed clauses removed: S is
satisfiable if and only if S’ is satisfiable.
Pure Literal Elimination
• A literal L is pure with regard to a clause set S if
and only if L is contained in at least one clause in
S, but L’ is not.
• A clause is pure with regard to a clause set S if
and only if it contains a pure literal.
• Obviously, with S any clause set, and with S’ the
clause set S with all pure clauses removed: S is
satisfiable if and only if S’ is satisfiable.
Unit Preference Resolution
• A unit clause is a clause that contains one
literal.
• Unit preference resolution tries to resolve
using unit clauses first.
Unit Literal Deletion and
Splitting
• For any clause set S, SL is the clause set that is
generated from S as follows:
– Remove all clauses from S that contain L.
– Remove all instances of L’ from all other clauses
• Obviously, with C = {L}  S, S is satisfiable if
and only if SL is satisfiable.
• It is also easy to see that for any clause set S, and
any literal L: S is satisfiable if and only if SL is
satisfiable or SL’ is satisfiable.
• The last observation suggests a splitting strategy
that forms the basis of Davis-Putnam.
Davis-Putnam
• Recursive routine Satisfiable(S) returns true iff S is
satisfiable:
boolean Satisfiable(S)
begin
if S = {} return true;
if S = {{}} return false;
select L  lit(S);
return Satisfiable(SL) || Satisfiable(SL’);
end
Making Davis-Putnam Efficient:
Adding Bells and Whistles
• The routine on the previous slide is not very
efficient. However, we can easily make it more
efficient:
–
–
–
–
return false as soon as {}S
add the unit rule: if {L}S return Satisfiable(SL)
strategically add deletion strategies
strategically choose the literal on which to split
• As far as I have gathered from the ATP literature,
such efficient Davis-Putnam routines are credited
to do well in comparison to other ATP routines.
Davis-Putnam as Trees
{P, Q}
{P, Q}
{P, Q}
{P, Q}
(P)
(P)
{Q}
{Q}
(Q)
{}
{Q}
{Q}
(Q)
{}
(Q)
{}
(Q)
{}
EG and ATP
• I will present 2 routines:
– 1. A decision procedure to decide on consistency
(satisfiability): this routine can be seen as a generalized
Davis-Putnam routine.
– 2. A routine to systematically derive a conclusion from
a set of premises, assuming that the conclusion is
logically entailed by the premises (if not, the routine
will stop, so you know that the conclusion is not
logically entailed). This routine is an extension of the
first routine.
Symbolization in EG
Expression in PL
Symbolization in EG
P
P
~










Inference Rules in EG
Double Cut

(De)Iteration
 
Erasure

Insertion




    



2k

1
2k+1 1





2k


1
2k+1 1
Unit Rule for EG
• Where L is a literal graph, and  any graph, the
procedure Unit(L, ), returns the graph  with all
occurrences of L removed, and with all
complements of L replaced with the empty cut.
Again, we’ll write this as L.
Gaining Efficiency by Avoiding
Clauses
A
B
B
Clausifying
DE (2x!)
A
A
B
B
C
B
C
C
C
No
Clausifying!
A
DC (2x!)
C
A
DE
B
C
DC
Satisfiability Decision Procedure
for EG
boolean Satisfiable(G)
begin
if G =
if G =
return true;
return false;
if G =
 
if G =   
return Satisfiable(   );
return Satisfiable(   );
if G =
L 
if G =
1 2
Satisfiable(
end
return Satisfiable(L);

return
1  ) || Satisfiable( 2  );
Satisfiability Example
E
A
C
C
A
D
B
C
) = Sat(
Sat(
A
B
D
D
B
E
B
B
Sat(
C
D
)=
C
D
C
B
D
) = Sat( D
D ) = Sat(
) = False
Adding Bells and Whistles
• Again, this procedure can be made a lot
more efficient by dealing with empty cuts,
double cuts, and duplicates more efficiently,
by various other deletion strategies, and by
strategically picking the subgraph on which
to split.
Satisfaction Graph
• A model is a list of literals where for each literal in
the list, its complement is not in the list.
• A satisfaction graph is a graph of the following
form:
M1
for n = 1:
for n = 0:

M
Mn
Routine for Transforming any
Graph into a Satisfaction Graph
graph Transform(G)
// when applicable, remove DC’s and duplicates
begin
if G =
or
if G =
L 
if G =
1  n
return G;
return Paste(L, Transform(L);

return
Transform( 1 ) 
end
Transform( n  )
U
Trans(
U
V
W
W
V
W
Trans(
U V
V
V
U
W
U
Trans( U
W U
W
U W
W
)
=
U
W
U
Trans( W W
U V
)=
W
V )=
U
)
=
U V W
Routine for Systematic
Derivations in EG
• Given any graphs  and , if  |= , then
the following routine systematically
transforms  into , using the inference
rules from EG:


DC




Trans



DC
IT(2x)
IN




DC
E
 
X Y
X Y
Sat(
)=
X Y
X Y
X
X Y
Sat(
Y
X Y
) | | Sat(
X Y
X Y
Sat( Y
Sat(
Y
) | | Sat(
X Y
) ||
Sat(
)
=
)
=
X Y
X
) = False | | False
X
= False
X Y
X Y
)=
Trans(
X Y
X
X Y
X Y
Trans(
)
X Y
X
Y
Trans(
X Y
Trans( Y
Y
X Y
X Y
)
Y
Trans(
=
)
=
)
=
X Y
X
X