From 2b3a0ef47c2d4d4ec94cc7a85bc49dfe39d42044 Mon Sep 17 00:00:00 2001
From: Brandon Rozek <brozek@brandonrozek.com>
Date: Mon, 27 Mar 2023 11:01:47 -0400
Subject: [PATCH] TPTP Examples

---
 Axioms/LIST-ROZEK.ax      | 58 +++++++++++++++++++++++++++++++++++++++
 Axioms/NUM-ROZEK.ax       | 42 ++++++++++++++++++++++++++++
 README.md                 | 37 +++++++++++++++++++++++++
 consequence_elimination.p | 18 ++++++++++++
 consistency_check.p       |  9 ++++++
 fof_conjecture.p          | 12 ++++++++
 question_answer.p         | 16 +++++++++++
 scripts/e_graph.sh        | 22 +++++++++++++++
 scripts/vampire_ce.sh     | 17 ++++++++++++
 scripts/vampire_qa.sh     | 17 ++++++++++++
 tf0_conjecture.p          |  9 ++++++
 tf0_induction.p           | 27 ++++++++++++++++++
 theory_conjecture.p       |  5 ++++
 13 files changed, 289 insertions(+)
 create mode 100644 Axioms/LIST-ROZEK.ax
 create mode 100644 Axioms/NUM-ROZEK.ax
 create mode 100644 README.md
 create mode 100644 consequence_elimination.p
 create mode 100644 consistency_check.p
 create mode 100644 fof_conjecture.p
 create mode 100644 question_answer.p
 create mode 100755 scripts/e_graph.sh
 create mode 100755 scripts/vampire_ce.sh
 create mode 100755 scripts/vampire_qa.sh
 create mode 100644 tf0_conjecture.p
 create mode 100644 tf0_induction.p
 create mode 100644 theory_conjecture.p

diff --git a/Axioms/LIST-ROZEK.ax b/Axioms/LIST-ROZEK.ax
new file mode 100644
index 0000000..c45deac
--- /dev/null
+++ b/Axioms/LIST-ROZEK.ax
@@ -0,0 +1,58 @@
+%--------------------------------------------------------------------------
+% File     : NUM-ROZEK : TPTP v8.1.2.
+% Domain   : Data Structures
+% Axioms   : Lists - Head, Tail, and Length
+%--------------------------------------------------------------------------
+
+%-- List Basics
+
+tff(list_t, type, list: $tType).
+
+tff(list_nil, type, nil : list).
+
+tff(list_cons, type,
+    cons: (
+        ($int * list) > list
+    )
+).
+
+%-- Head
+
+tff(head_t, type,
+    head: list > $int
+).
+
+tff(head_cons, axiom,
+    ![H: $int, T: list]: (
+        head(cons(H, T)) = H
+    )
+).
+
+%-- Tail
+
+tff(tail_t, type,
+    tail: list > list
+).
+
+tff(tail_cons, axiom,
+    ![H: $int, T: list]: (
+        tail(cons(H, T)) = T
+    )
+).
+
+% Note: The existence of head and tail definition shows that
+% cons is injective.
+
+%-- Length
+
+tff(length_t, type,
+    length: list > $int
+).
+
+tff(length_nil, axiom, length(nil) = 0).
+
+tff(length_cons, axiom,
+    ![H: $int, T: list]: (
+        length(cons(H, T)) = $sum(1, length(T))
+    )
+).
diff --git a/Axioms/NUM-ROZEK.ax b/Axioms/NUM-ROZEK.ax
new file mode 100644
index 0000000..44f6c2e
--- /dev/null
+++ b/Axioms/NUM-ROZEK.ax
@@ -0,0 +1,42 @@
+%--------------------------------------------------------------------------
+% File     : NUM-ROZEK : TPTP v8.1.2.
+% Domain   : Number Theory
+% Axioms   : Number theory - Equality and Addition
+%--------------------------------------------------------------------------
+
+%-- Constants
+fof(c1, axiom, "one" = successor("zero")).
+fof(c1, axiom, "two" = successor("one")).
+fof(c1, axiom, "three" = successor("two")).
+fof(c1, axiom, "four" = successor("three")).
+fof(c1, axiom, "five" = successor("four")).
+
+%-- Equality with respect to natural numbers
+
+fof(zero, axiom,
+    ![X] : "zero" != successor(X)
+).
+
+fof(successor_equality, axiom,
+    ![A, B]: (
+        (successor(A) = successor(B)) =>
+        (A = B)
+    )
+).
+% Note: Also shows that successor is an injective function
+
+%-- Addition Axioms
+
+fof(adding_zero, axiom,
+    ![A]: add(A,"zero") = A
+).
+
+fof(addition, axiom,
+    ![A, B]:
+        (add(A,successor(B)) =
+        successor(add(A,B)))
+).
+
+
+
+%--------------------------------------------------------------------------
\ No newline at end of file
diff --git a/README.md b/README.md
new file mode 100644
index 0000000..6f9872e
--- /dev/null
+++ b/README.md
@@ -0,0 +1,37 @@
+# TPTP Example Files
+
+This repository contains the example files given during my talk on "Automated Theorem Proving with TPTP". In that talk, I demonstrated creating axiom and problem files and showcased how to run them using both the Vampire and E automated theorem provers.
+
+## Axioms
+
+Within `Axioms/NUM-ROZEK.ax` are a few simple axioms describing natural numbers using the successor formalism. It describes both natural number equality and addition.
+
+The file `Axioms/LIST-ROZEK.ax` contains the `cons` representation of a list data structure. It also has a definition of a length of a list.
+
+## Problems
+
+### Conjectures
+
+There are four examples of conjectures in this repository.
+- `fof_conjecture.p` : Contains a number theory problem axiomatized by a custom file and represented via non-typed first order formulae.
+- `theory_conjecture.p` : Contains a number theory problem axiomatized by the theorem prover's internal theory of integers and reprsented via typed first order formulae.
+- `tf0_conjecture.p` : Contains a data structure problem axiomatized by a custom file and represented via typed first order formulae.
+- `tf0_induction.p` : Same as `tf0_conjecture.p` but contains an example of induction using a first-order induction axiom.
+
+### Special Modes
+
+*Question-Answering* is as of the time of writing an in-progress specification. Therefore, to activate it within Vampire you'll need to specify extra flags. See `scripts/vampire_qa.sh` for details.
+
+Question-Answering within E does not require special flags but does require the role of the problem to be of type `question` instead of `conjecture`.
+
+Vampire supports *consequence-elimination* which determines which formulas are already deducible from a set of axioms. This requires setup in both the problem file and in the command flags you provide. Within the problem file, you need to set the potential redundant formula's role to `claim` and see `scripts/vampire_ce.sh` for the CLI flags.
+
+Consistency checking is an instance of the standard conjecture problems except you're trying to derive falsity. This is represented as `$false` within TPTP.
+
+## Issues?
+
+For a few of the problems, the default search strategy within Vampire won't be able to find the solution. In those cases, activating competition mode often helps. This mode tries multiple strategies within your time limit.
+
+```bash
+vampire --mode casc PROBLEM_FILE.p
+```
diff --git a/consequence_elimination.p b/consequence_elimination.p
new file mode 100644
index 0000000..662574b
--- /dev/null
+++ b/consequence_elimination.p
@@ -0,0 +1,18 @@
+include('Axioms/NUM-ROZEK.ax').
+
+fof(c2, claim,
+    ![X] : (successor(X) != "zero")
+).
+
+fof(c3, claim, "two" = sucessor(successor("zero"))).
+
+fof(c4, claim,
+    ![A, B]: (
+        (successor(successor(A)) = successor(B)) =>
+        (successor(A) = B)
+    )
+).
+
+fof(c5, claim,
+    "zero" = add("zero", "zero")
+).
diff --git a/consistency_check.p b/consistency_check.p
new file mode 100644
index 0000000..35d91ed
--- /dev/null
+++ b/consistency_check.p
@@ -0,0 +1,9 @@
+fof(lt_irreflex, axiom,
+    ![X] : (~lt(X, X))
+).
+
+fof(lt_assym, axiom,
+    ![X, Y] : (lt(X, Y) <=> ~lt(Y, X))
+).
+
+fof(prove, conjecture, $false).
diff --git a/fof_conjecture.p b/fof_conjecture.p
new file mode 100644
index 0000000..d8e5023
--- /dev/null
+++ b/fof_conjecture.p
@@ -0,0 +1,12 @@
+include('Axioms/NUM-ROZEK.ax').
+
+%-- Define Even
+fof(h1, hypothesis, even("zero")).
+fof(h2, hypothesis,
+    ![X] : (even(X) => even(add(X, "two")))
+).
+
+%-- Problem
+fof(c1, conjecture,
+    ![X] : (even(X) => even(add(X, "four")))
+).
diff --git a/question_answer.p b/question_answer.p
new file mode 100644
index 0000000..d8de3e4
--- /dev/null
+++ b/question_answer.p
@@ -0,0 +1,16 @@
+include('Axioms/NUM-ROZEK.ax').
+
+fof(previous_answers, hypothesis,
+    ![X, Y]: (previous(X, Y) <=>
+    (
+        (X = "three" & Y = "zero") |
+        (X = "zero" & Y = "three")
+    )
+)).
+
+fof(goal, question,
+    ?[X, Y]: (
+        (add(X, Y) = "three") &
+        ~previous(X, Y)
+    )
+).
diff --git a/scripts/e_graph.sh b/scripts/e_graph.sh
new file mode 100755
index 0000000..d1eceea
--- /dev/null
+++ b/scripts/e_graph.sh
@@ -0,0 +1,22 @@
+#!/bin/sh
+
+# ProofGraph Output via E Prover
+
+show_usage() {
+    echo "Usage: e_graph [problem_file]"
+    exit 1
+}
+
+# Check argument count
+if [ "$#" -ne 1 ]; then
+    show_usage
+fi
+
+# Use E Prover to produce a proof graph via GraphViz dot format
+eprover --proof-graph=1 -l 0 "$1" > example_proofgraph.dot
+
+# Use GraphVis to create a postscript file from the dot format
+dot -Tps example_proofgraph.dot -o proof_graph.ps
+
+# Cleanup
+rm e.dot
diff --git a/scripts/vampire_ce.sh b/scripts/vampire_ce.sh
new file mode 100755
index 0000000..b115a15
--- /dev/null
+++ b/scripts/vampire_ce.sh
@@ -0,0 +1,17 @@
+#!/bin/sh
+
+# Consequence Elimination via Vampire
+
+show_usage() {
+    echo "Usage: vampire_ce [problem_file]"
+    exit 1
+}
+
+# Check argument count
+if [ "$#" -ne 1 ]; then
+    show_usage
+fi
+
+# Note: Disables avatar mode (av) which uses a Z3 solver.
+
+vampire -av off --mode consequence_elimination "$1"
diff --git a/scripts/vampire_qa.sh b/scripts/vampire_qa.sh
new file mode 100755
index 0000000..b84dd32
--- /dev/null
+++ b/scripts/vampire_qa.sh
@@ -0,0 +1,17 @@
+#!/bin/sh
+
+# Question Answering using Vampire
+
+show_usage() {
+    echo "Usage: vampire_qa [problem_file]"
+    exit 1
+}
+
+# Check argument count
+if [ "$#" -ne 1 ]; then
+    show_usage
+fi
+
+# Note: Disables avatar mode (av) which uses a Z3 solver.
+
+vampire -av off -qa answer_literal "$1"
diff --git a/tf0_conjecture.p b/tf0_conjecture.p
new file mode 100644
index 0000000..9a0c271
--- /dev/null
+++ b/tf0_conjecture.p
@@ -0,0 +1,9 @@
+include('Axioms/LIST-ROZEK.ax').
+
+% Problem
+
+tff(injective, conjecture,
+    ![H1: $int, H2: $int, T1: list, T2: list] : (
+        (cons(H1, T1) = cons(H2, T2)) => ((H1 = H2) & (T1 = T2))
+    )
+).
diff --git a/tf0_induction.p b/tf0_induction.p
new file mode 100644
index 0000000..ffafcfb
--- /dev/null
+++ b/tf0_induction.p
@@ -0,0 +1,27 @@
+include('Axioms/LIST-ROZEK.ax').
+
+% Definition
+tff(gezero_t, type, gezero: list > $o).
+
+tff(gezero, axiom,
+    ![L: list]: (gezero(L) <=> $greatereq(length(L), 0))
+).
+
+% Induction Axiom
+
+tff(gezero_induction, axiom,
+    (gezero(nil) &
+    ![H: $int, T: list]: (
+        gezero(T) => gezero(cons(H, T))
+    ))
+    =>
+    ![L: list]: (
+        gezero(L)
+    )
+).
+
+% Problem
+
+tff(goal, conjecture,
+    ![L: list]: gezero(L)
+).
diff --git a/theory_conjecture.p b/theory_conjecture.p
new file mode 100644
index 0000000..b1efe56
--- /dev/null
+++ b/theory_conjecture.p
@@ -0,0 +1,5 @@
+tff(goal, conjecture,
+    ![X: $int] : (
+        $greater(X, 1) => $greater($product(X, X), X)
+    )
+).