1 files changed, 116 insertions, 0 deletions
diff --git a/proofs/signatures/example.plf b/proofs/signatures/example.plf
new file mode 100755
index 000000000..5df1f31c3
--- /dev/null
+++ b/proofs/signatures/example.plf
@@ -0,0 +1,116 @@
+; to check, run : lfsc sat.plf smt.plf th_base.plf example.plf
+
+; -------------------------------------------------------------------------------- 
+; input :
+; ( a = b )
+; ( b = f(c) )
+; ( a != f(c) V a != b )
+
+; theory lemma (by transitivity) :
+; ( a != b V b != f(c) V a = f(c) )
+
+
+;  With the theory lemma, the input is unsatisfiable.
+; -------------------------------------------------------------------------------- 
+
+
+
+(check 
+(% s sort
+(% a (term s)
+(% b (term s)
+(% c (term s)
+(% f (term (arrow s s))
+
+; -------------------- declaration of input formula -----------------------------------
+
+(% A1 (th_holds (= s a b))
+(% A2 (th_holds (= s b (apply _ _ f c)))
+(% A3 (th_holds (or (not (= s a (apply _ _ f c))) (not (= s a b))))
+
+
+; ------------------- specify that the following is a proof of the empty clause -----------------
+
+(: (holds cln)
+
+; ---------- use atoms (a1, a2, a3) to map theory literals to boolean literals (v1, v2, v3) ------
+
+(decl_atom (= s a b) (\ v1 (\ a1
+(decl_atom (= s b (apply _ _ f c)) (\ v2 (\ a2
+(decl_atom (= s a (apply _ _ f c)) (\ v3 (\ a3
+
+
+; --------------------------- proof of theory lemma ---------------------------------------------
+
+(satlem _ _
+(ast _ _ _ a1 (\ l1
+(ast _ _ _ a2 (\ l2
+(asf _ _ _ a3 (\ l3
+(clausify_false
+
+; this should be a proof of l1 ^ l2 ^ ~l3 => false
+; this is done by theory proof rules (currently just use "trust")
+
+  trust
+
+))))))) (\ CT
+; CT is the clause ( ~v1 V ~v2 V v3 )
+
+; -------------------- clausification of input formulas -----------------------------------------
+
+(satlem _ _
+(asf _ _ _ a1 (\ l1
+(clausify_false
+
+; input formula A1 is ( ~l1 )
+; the following should be a proof of l1 ^ ( ~l1 ) => false
+; this is done by natural deduction rules
+
+  (contra _ A1 l1)
+
+))) (\ C1
+; C1 is the clause ( v1 )
+
+
+(satlem _ _
+(asf _ _ _ a2 (\ l2
+(clausify_false
+
+; input formula A2 is ( ~l2 )
+; the following should be a proof of l2 ^ ( ~l2 ) => false
+; this is done by natural deduction rules
+
+   (contra _ A2 l2)
+   
+))) (\ C2 
+; C2 is the clause ( v2 )
+
+
+(satlem _ _
+(ast _ _ _ a3 (\ l3
+(ast _ _ _ a1 (\ l1
+(clausify_false
+
+; input formula A3 is ( ~a3 V ~a1 ) 
+; the following should be a proof of a3 ^ a1 ^ ( ~a3 V ~a1 ) => false
+; this is done by natural deduction rules
+
+  (contra _ l1 (or_elim_1 _ _ (not_not_intro _ l3) A3))
+
+))))) (\ C3  
+; C3 is the clause ( ~v3 V ~v1 )
+
+
+
+; -------------------- resolution proof ------------------------------------------------------------
+
+(satlem_simplify _ _ _ 
+
+(R _ _ C1
+(R _ _ C2
+(R _ _ CT C3 v3) v2) v1)
+
+(\ x x))
+
+))))))))))))))))))))))))))
+)
+\ No newline at end of file