feat: implement command-line interface and add end-to-end propositional logic test suite

1 files changed, 5 insertions, 5 deletions

diff --git a/proofsearch/src/proof/proof_trace.cc b/proofsearch/src/proof/proof_trace.cc
index b1b4343..fff54a3 100644
--- a/proofsearch/src/proof/proof_trace.cc
+++ b/proofsearch/src/proof/proof_trace.cc
@@ -30,7 +30,7 @@
 
 namespace atp {
 
-// ─── extractProof ────────────────────────────────────────────────────────────
+// ─── extractProof 
 // DFS from empty clause back to axioms, collect all participating clauses,
 // then reverse for topological order (axioms first).
 
@@ -71,7 +71,7 @@ std::vector<ProofStep> extractProof(const ClauseStore& store, ClauseId empty_cla
     return steps;
 }
 
-// ─── termToString ────────────────────────────────────────────────────────────
+// ─── termToString 
 
 std::string termToString(TermId id, const TermBank& bank) {
     const Term& t = bank.getTerm(id);
@@ -92,7 +92,7 @@ std::string termToString(TermId id, const TermBank& bank) {
     return result;
 }
 
-// ─── clauseToString ──────────────────────────────────────────────────────────
+// ─── clauseToString 
 
 std::string clauseToString(const Clause& clause, const TermBank& bank) {
     if (clause.isEmpty()) {
@@ -112,7 +112,7 @@ std::string clauseToString(const Clause& clause, const TermBank& bank) {
     return result;
 }
 
-// ─── ruleToString ────────────────────────────────────────────────────────────
+// ─── ruleToString 
 
 static std::string ruleToString(InferenceRule rule) {
     switch (rule) {
@@ -123,7 +123,7 @@ static std::string ruleToString(InferenceRule rule) {
     }
 }
 
-// ─── formatProof ─────────────────────────────────────────────────────────────
+// ─── formatProof 
 
 std::string formatProof(const std::vector<ProofStep>& proof,
                         const ClauseStore& store, const TermBank& bank) {