From 7e0ac10b7b58de84910f0d4bb0d05cf36edeba2b Mon Sep 17 00:00:00 2001 From: Richard Qin Date: Sat, 4 Apr 2026 04:56:51 +0800 Subject: feat: implement command-line interface and add end-to-end propositional logic test suite --- proofsearch/data/simple_propositional.p | 5 +++++ 1 file changed, 5 insertions(+) create mode 100644 proofsearch/data/simple_propositional.p (limited to 'proofsearch/data/simple_propositional.p') diff --git a/proofsearch/data/simple_propositional.p b/proofsearch/data/simple_propositional.p new file mode 100644 index 0000000..283c326 --- /dev/null +++ b/proofsearch/data/simple_propositional.p @@ -0,0 +1,5 @@ +% Simple propositional-style test +% P(a) and (P(X) → Q(X)) and ¬Q(a) should be unsatisfiable. +cnf(fact, axiom, p(a)). +cnf(rule, axiom, ~p(X) | q(X)). +cnf(goal, negated_conjecture, ~q(a)). -- cgit v1.2.3