TPTP Examples

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))
+    )
+).

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)))
+).
+
+
+
+%--------------------------------------------------------------------------

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
+```

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")
+).

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).

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")))
+).

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)
+    )
+).

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

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"

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"

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))
+    )
+).

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)
+).

theory_conjecture.p

@@ -0,0 +1,5 @@
+tff(goal, conjecture,
+    ![X: $int] : (
+        $greater(X, 1) => $greater($product(X, X), X)
+    )
+).