1 ///////////////////////////////////////////////////////////////////////////////
3 // This example program performs simplification of first order logic
4 // formulas using rewriting. We'll use topdown rules for this.
6 ///////////////////////////////////////////////////////////////////////////////
8 #include <AD/strings/quark.h>
9 #include <AD/generic/generic.h>
11 datatype Wff = T => "true"
14 | And Wff, Wff => '(' _ "and" _ ')'
15 | Or Wff, Wff => '(' _ "or" _ ')'
16 | Not Wff => "not" '(' _ ')'
17 | Implies Wff, Wff => '(' _ "=>" _ ')'
18 | Predicate Id, Ids => _ _
19 | Exists Id, Wff => "exists" _ '.' _
20 | Forall Id, Wff => "forall" _ '.' _
21 and Ids :: printable = #() | #( Id ... Ids )
22 where type Id = class Quark
25 ///////////////////////////////////////////////////////////////////////////////
27 // Function to check that an identifier occurs free in a wff.
29 ///////////////////////////////////////////////////////////////////////////////
30 Bool is_free (Id id, Wff wff)
32 { T || F: { return true; }
33 | Var x: { return id != x; }
34 | And(a,b): { return is_free(id,a) && is_free(id,b); }
35 | Or(a,b): { return is_free(id,a) && is_free(id,b); }
36 | Implies(a,b): { return is_free(id,a) && is_free(id,b); }
37 | Not a: { return is_free(id,a); }
38 | Exists(a,b): { return a == id || is_free(id,b); }
39 | Forall(a,b): { return a == id || is_free(id,b); }
40 | Predicate(_,l): { Ids ids = l;
42 { #(): { return true; }
43 | #(x ... _) | x == id: { return false; }
44 | #(_ ... t): { ids = t; }
50 instantiate datatype Wff, Ids;
52 void transform(Wff wff)
54 cout << "Input: " << wff << endl;
56 rewrite (wff) type (Wff)
60 // Transform into prenex normal form
62 Forall(x,Not(P)): Not(Exists(x,P))
63 | Exists(x,Not(P)): Not(Forall(x,P))
64 | Forall(x,And(P,Q)): And(Forall(x,P),Forall(x,Q))
65 | Exists(x,Or(P,Q)): Or(Exists(x,P),Exists(x,Q))
66 | Exists(x,And(P,Q)) | is_free(x,Q): And(Exists(x,P),Q)
67 | Exists(x,And(P,Q)) | is_free(x,P): And(P,Exists(x,Q))
68 | Forall(x,Or(P,Q)) | is_free(x,Q): Or(Forall(x,P),Q)
69 | Forall(x,Or(P,Q)) | is_free(x,P): Or(P,Forall(x,Q))
70 | Forall(x,P) | is_free(x,P): P
71 | Exists(x,P) | is_free(x,P): P
84 | Implies(X,Y): Or(Not(X),Y)
87 cout << "Output: " << wff << endl;
95 wff = Implies(Exists(#"w",Forall(#"x",Predicate(#"P",#(#"w",#"x")))),
96 Forall(#"y",Exists(#"z",Predicate(#"P",#(#"z",#"y")))));
99 wff = Forall(#"w",Forall(#"y",Exists(#"x",Exists(#"z",
100 Implies(Predicate(#"P",#(#"w",#"x")),
101 Predicate(#"P",#(#"z",#"y")))))));
103 wff = Forall(#"w",Forall(#"y",Exists(#"x",
104 Implies(Predicate(#"P",#(#"w",#"x")),
105 Predicate(#"P",#(#"x",#"y"))))));