From 761a18c4f960423ae672350174ff19ff5eb4bbb0 Mon Sep 17 00:00:00 2001
From: mehbark <terezi@pyrope.net>
Date: Thu, 20 Feb 2025 22:26:09 -0500
Subject: [PATCH] crud to remove

---
 formal.scm | 95 ++++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 95 insertions(+)
 create mode 100644 formal.scm

diff --git a/formal.scm b/formal.scm
new file mode 100644
index 0000000..bd05012
--- /dev/null
+++ b/formal.scm
@@ -0,0 +1,95 @@
+;; (equal? (make-pand 1 2) (make-pand 1 2)) => #f
+(define (make-pand p q) `(and ,p ,q))
+
+(define pand
+  (case-lambda
+    [() #t]
+    [(p) p]
+    [(p . qs) (fold-left make-pand p qs)]))
+
+(define (make-por p q) `(or ,p ,q))
+
+(define por
+  (case-lambda
+    [() #f]
+    [(p) p]
+    [(p . qs) (fold-left make-por p qs)]))
+
+;; iirc, or: (not p) or q
+(define (make-p-> p q) `(-> ,p ,q))
+
+;; could fold but laziness
+(define p->
+  (case-lambda
+    [() #t]
+    [(p) p]
+    [(p . qs) (make-p-> p (apply p-> qs))]))
+
+(define (p<-> p q) (pand (p-> p q) (p-> q p)))
+;; maybe could have some pretty-printing logic? this definition is just 2 good 2 pass up
+(define (pnot p) (p-> p #f))
+(define ~ pnot)
+
+;; maybe a var is just a sym? no forall lel
+;; existence l8r
+;; nah
+;; valued vars? :o
+
+;; (define-record-type forall
+;;   (fields vars p)
+;;   (nongenerative forall))
+;; (define-syntax forall
+;;   (syntax-rules ()
+;;     [(forall (var* ...) p)
+;;      (make-forall
+;;       '(var* ...)
+;;       (let ([var* 'var*] ...) p))]
+;;     [(forall var p) (forall (var) p)]))
+
+(define-record-type argument
+  (fields premises conclusion)
+  (nongenerative argument))
+
+(define-syntax argument
+  (syntax-rules ()
+    [(_ (var* ...) (premise* ...) conclusion)
+     (lambda (var* ...)
+       (make-argument (list premise* ...) conclusion))]))
+
+(define modus-ponens
+  (argument (p q)
+    ((p-> p q)
+     p)
+    q))
+
+(define modus-tollens
+  (argument (p q)
+    ((p-> p q)
+     (~ q))
+    (~ p)))
+
+;; (follows (P* ... (-> p q) p Q* ...) q modus-ponens) => #t
+;; iterative argument
+;; laws of inference are taken as fact
+;; norm vars
+;; order irrelevant
+;; search for reqs?
+
+(define (premises<=? p1 p2)
+  (and (andmap (lambda (prem) (member prem p2)) p1)
+       #t))
+
+(define (follows? p q by)
+  (and (equal? q (argument-conclusion by))
+       (premises<=? (argument-premises by) p)))
+
+(define (argument-extend arg rule)
+  (if (premises<=? (argument-premises rule) (argument-premises arg))
+      (make-argument )))
+
+
+
+
+(define-record-type proof-state
+  (fields knowns goals)
+  (nongenerative proof-state))