alc-in-snark.lisp

(ql:quickload :snark)

(initialize)
(use-resolution t)

(defun var-complemente (var)
  (if (equal var '?x)
      '?y
      '?x))

(defun translate (var concept)
  (if (symbolp concept)
      `(,concept ,var)
      (let ((op (car concept))
	    (re (cdr concept)))
	(case op
	  (and `(and ,(translate var (car re))
		     ,(translate var (cadr re))))
	  (or `(or ,(translate var (car re))
		   ,(translate var (cadr re))))
	  (not `(not ,(translate var (car re))))
	  (forall `(forall (,(var-complemente var))
			   (implies (,(car re) ,var ,(var-complemente var))
				    ,(translate (var-complemente var) (cadr re)))))
	  (exists `(exists (,(var-complemente var))
			   (and (,(car re) ,var ,(var-complemente var))
				,(translate (var-complemente var) (cadr re)))))))))


(prove `(forall (?x)
		(implies ,(translate '?x '(and (exists h A) (forall h C)))
			 ,(translate '?x '(exists h C)))))

;; running

SNARK-USER> (initialize)
; Running SNARK from /Users/arademaker/quicklisp/dists/quicklisp/software/snark-20160421-git/ in SBCL 1.3.18 (64-bit) on urca.wireless.l3.nuigalway.ie at 2017-06-20T07:32:09
NIL
SNARK-USER> (use-resolution t)
T
SNARK-USER> `(forall (?x)
		     (implies ,(translate '?x '(and (exists h A) (forall h C)))
			      ,(translate '?x '(exists h C))))
(FORALL (?X)
 (IMPLIES
  (AND (EXISTS (?Y) (AND (H ?X ?Y) (A ?Y)))
       (FORALL (?Y) (IMPLIES (H ?X ?Y) (C ?Y))))
  (EXISTS (?Y) (AND (H ?X ?Y) (C ?Y)))))
SNARK-USER> (prove `(forall (?x)
			    (implies ,(translate '?x '(and (exists h A) (forall h C)))
				     ,(translate '?x '(exists h C)))))
; The current SNARK option values are
;    (USE-RESOLUTION T)
;       (USE-HYPERRESOLUTION NIL)
;       (USE-NEGATIVE-HYPERRESOLUTION NIL)
;       (USE-UR-RESOLUTION NIL)
;       (USE-UR-PTTP NIL)
;       (USE-PARAMODULATION NIL)
;       (USE-FACTORING NIL)
;       (USE-EQUALITY-FACTORING NIL)
;       (USE-CONDENSING T)
;       (USE-RESOLVE-CODE NIL)
;       (USE-UNIT-RESTRICTION NIL)
;       (USE-INPUT-RESTRICTION NIL)
;       (USE-LITERAL-ORDERING-WITH-RESOLUTION NIL)
;       (USE-LITERAL-ORDERING-WITH-HYPERRESOLUTION NIL)
;       (USE-LITERAL-ORDERING-WITH-NEGATIVE-HYPERRESOLUTION NIL)
;       (USE-LITERAL-ORDERING-WITH-UR-RESOLUTION NIL)
;       (USE-LITERAL-ORDERING-WITH-PARAMODULATION NIL)
;       (USE-SUBSUMPTION T)
;       (USE-SUBSUMPTION-BY-FALSE :FALSE)
;       (USE-SIMPLIFICATION-BY-UNITS T)
;       (USE-SIMPLIFICATION-BY-EQUALITIES T)
;       (USE-TERM-ORDERING :RPO)
;       (USE-DEFAULT-ORDERING T)
;       (1-ARY-FUNCTIONS>2-ARY-FUNCTIONS-IN-DEFAULT-ORDERING NIL)
;       (ORDERING-FUNCTIONS>CONSTANTS NIL)
;       (RPO-STATUS :MULTISET)
;       (KBO-STATUS :LEFT-TO-RIGHT)
;       (USE-INDEFINITE-ANSWERS NIL)
;       (USE-CONDITIONAL-ANSWER-CREATION NIL)
;       (USE-CONSTRAINT-SOLVER-IN-SUBSUMPTION NIL)
;       (ALLOW-SKOLEM-SYMBOLS-IN-ANSWERS T)
;       (REWRITE-ANSWERS NIL)
;       (USE-CONSTRAINT-PURIFICATION NIL)
;       (USE-FUNCTION-CREATION NIL)
;       (USE-REPLACEMENT-RESOLUTION-WITH-X=X NIL)
;       (USE-PARAMODULATION-ONLY-INTO-UNITS NIL)
;       (USE-PARAMODULATION-ONLY-FROM-UNITS NIL)
;       (USE-SINGLE-REPLACEMENT-PARAMODULATION NIL)
;       (ASSERT-CONTEXT :ROOT)
;       (ASSERT-SUPPORTED T)
;       (ASSUME-SUPPORTED T)
;       (PROVE-SUPPORTED T)
;       (ASSERT-SEQUENTIAL NIL)
;       (ASSUME-SEQUENTIAL NIL)
;       (PROVE-SEQUENTIAL NIL)
;       (NUMBER-OF-GIVEN-ROWS-LIMIT NIL)
;       (NUMBER-OF-ROWS-LIMIT NIL)
;       (AGENDA-LENGTH-BEFORE-SIMPLIFICATION-LIMIT 10000)
;       (AGENDA-LENGTH-LIMIT 3000)
;       (RUN-TIME-LIMIT NIL)
;       (ROW-WEIGHT-LIMIT NIL)
;       (ROW-WEIGHT-BEFORE-SIMPLIFICATION-LIMIT NIL)
;       (LEVEL-PREF-FOR-GIVING NIL)
;       (AGENDA-ORDERING-FUNCTION ROW-PRIORITY)
;       (PRUNING-TESTS (ROW-WEIGHT-LIMIT-EXCEEDED))
;       (PRUNING-TESTS-BEFORE-SIMPLIFICATION (ROW-WEIGHT-BEFORE-SIMPLIFICATION-LIMIT-EXCEEDED))
;       (USE-CLAUSIFICATION T)
;       (USE-EQUALITY-ELIMINATION NIL)
;       (USE-MAGIC-TRANSFORMATION NIL)
;       (USE-AC-CONNECTIVES T)
;       (USE-PURITY-TEST NIL)
;       (USE-RELEVANCE-TEST NIL)

(Row 1
   (H SKOLEMDDSS1 SKOLEMDDSS2)
   NEGATED_CONJECTURE) 
(Row 2
   (A SKOLEMDDSS2)
   NEGATED_CONJECTURE) 
(Row 3
   (OR (NOT (H SKOLEMDDSS1 ?X)) (C ?X))
   NEGATED_CONJECTURE) 
(Row 4
   (OR (NOT (H SKOLEMDDSS1 ?X)) (NOT (C ?X)))
   NEGATED_CONJECTURE) 
(Row 5
   (C SKOLEMDDSS2)
   (RESOLVE 3 1)) 
(Row 6
   FALSE
   (REWRITE (RESOLVE 4 1) 5)) 

(Refutation
(Row 1
   (H SKOLEMDDSS1 SKOLEMDDSS2)
   NEGATED_CONJECTURE)
(Row 3
   (OR (NOT (H SKOLEMDDSS1 ?X)) (C ?X))
   NEGATED_CONJECTURE)
(Row 4
   (OR (NOT (H SKOLEMDDSS1 ?X)) (NOT (C ?X)))
   NEGATED_CONJECTURE)
(Row 5
   (C SKOLEMDDSS2)
   (RESOLVE 3 1))
(Row 6
   FALSE
   (REWRITE (RESOLVE 4 1) 5))
)

; Summary of computation:
;         7 formulas have been input or derived (from 5 formulas).
;         6 (86%) were retained.  Of these,
;            6 (100%) are still being kept.
; 
; Run time in seconds excluding printing time:
;     0.000   0%   Assert                       (1 call)
;     0.000   0%   Process new row              (6 calls)
;     0.000   0%   Resolution                   (4 calls)
;     0.000   0%   Condensing                   (2 calls)
;     0.000   0%   Forward subsumption          (2 calls)
;     0.000   0%   Backward subsumption         (2 calls)
;     0.000   0%   Forward simplification       (6 calls)
;     0.001   0%   Backward simplification      (6 calls)
;     0.000   0%   Sortal reasoning             (26 calls)
;     0.379 100%   Other
;     0.380        Total
;    24.432        Real time
; 
; Term-hash-array has 5 terms in all.
; Feature-vector-row-index has 2 entries (2 at peak, 2 added, 0 deleted).
; Feature-vector-row-index has 7 nodes (7 at peak, 7 added, 0 deleted).
;  Retrieved 0 possibly forward subsuming rows in 2 calls.
;  Retrieved 0 possibly backward subsumed rows in 2 calls.
; Path-index has 7 entries (7 at peak, 7 added, 0 deleted).
; Path-index has 14 nodes (14 at peak, 14 added, 0 deleted).
; Trie-index has 7 entries (7 at peak, 7 added, 0 deleted).
; Trie-index has 12 nodes (12 at peak, 12 added, 0 deleted).
; Retrieved 1 generalization term in 3 calls.
; Retrieved 3 instance terms in 3 calls.
; Retrieved 6 unifiable terms in 6 calls.
; 
; The agenda of rows to process has 1 entry:
;     1 with value 5
; The agenda of rows to give has 1 entry:
;     1 with value (4 4)
:PROOF-FOUND
SNARK-USER>