1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
|
;; Sequence Calculus in miniKanren
;;
;; To run this, you will need a copy of
;; https://github.com/webyrd/miniKanren-with-symbolic-constraints
;; (assumed to be in miniKanren from here on)
;;
;; To prove or disprove something:
;; guile -l miniKanren/mk-guile.scm -e prove -s sequentcalc.scm "'()" "'(or a (not b))"
;;
;; To query for valid statements, run the guile repl:
;; $ guile -l miniKanren/mk-guile.scm -l sequentcalc.scm
;; ;; what should q be to make ⇒ a ∧ ¬ q valid? (up to 10 results)
;; scheme@(guile-user)> (run 10 (q) (sequent '() `(or a (not ,q))))
;; ;; what could p,q be to make p ⇒ q true? (up to 10 results)
;; scheme@(guile-user)> (run 10 (p q) (sequent p q))
;;
;; Note that (run*) should usually be avoided, since it will almost
;; always not terminate (as there are usually an infinite amount
;; of possible completions).
;; goal: is q a member of the list l?
(define
(membero q l)
(fresh (x xs)
(== l `(,x . ,xs))
(conde
((== q x))
((membero q xs)))))
;; goal: list l only contains q
(define (onlo q l)
(conde ((== l '()))
((fresh (x xs)
(== l `(,x . ,xs))
(== x q)
(onlo q xs)))))
;; goal: rest = l with all instances of q removed
(define (removo q l rest)
(conde
((== rest '()) (onlo q l))
((absento q rest) (== rest l))
((fresh (x xs r rs)
(== l `(,x . ,xs))
(== rest `(,r . ,rs))
(conde
((== q x) (=/= q r) (removo q xs `(,r . ,rs)))
((=/= q x) (== x r) (removo q xs rs)))))))
(define (sequent gamma delta)
(conde
;; the base axiom: a,Γ ⇒ a,Δ
((fresh (a) (membero a gamma) (membero a delta)))
;; the not axiom: ⊥,Γ ⇒ Δ
((membero 'bottom gamma))
;; the not left rule
((fresh (f)
;; there is ¬F on the left side
(membero `(not ,f) gamma)
;; prove that Γ ⇒ F,Δ
(fresh (g) (removo `(not ,f) gamma g) (sequent g `(,f . ,delta)))))
;; the not right rule
((fresh (f)
(membero `(not ,f) delta)
(fresh (d) (removo `(not ,f) delta d) (sequent `(,f . ,gamma) d))))
;; the and left rule
((fresh (a b)
(membero `(and ,a ,b) gamma)
(fresh (g)
(removo `(and ,a ,b) gamma g)
(sequent `(,a . (,b . ,g)) delta))))
;; the and right rule
((fresh (a b)
(membero `(and ,a ,b) delta)
(fresh (d)
(removo `(and ,a ,b) delta d)
(sequent gamma `(,a . ,d))
(sequent gamma `(,b . ,d)))))
;; the left or rule
((fresh (a b)
(membero `(or ,a ,b) gamma)
(fresh (g)
(removo `(or ,a ,b) gamma g)
(sequent `(,a . ,g) delta)
(sequent `(,b . ,g) delta))))
;; the right or rule
((fresh (a b)
(membero `(or ,a ,b) delta)
(fresh (d)
(removo `(or ,a ,b) delta d)
(sequent gamma `(,a . (,b . ,d))))))
;; the left arrow rule
((fresh (a b)
(membero `(arrow ,a ,b) gamma)
(fresh (g)
(removo `(arrow ,a ,b) gamma g)
(sequent g `(,a . ,delta))
(sequent `(,b . ,g) delta))))
;; the right arrow rule
((fresh (a b)
(membero `(arrow ,a ,b) delta)
(fresh (d)
(removo `(arrow ,a ,b) delta d)
(sequent `(a . ,gamma) `(,b . ,d)))))))
(define (prove args)
(let ((gamma (eval-string (car (cdr args))))
(delta (eval-string (car (cdr (cdr args))))))
(if (equal? '() (run 1 (q) (sequent gamma delta)))
(display "does not follow from sequent calculus")
(display "follows from sequent calculus"))
(newline)))
|
