Automated Theorem Proving
 TPTP
 Systems
 Imandra
 Strategies
 Methodology
 Literal Selection
 Term Indexing
 Theories
 Higher Order
 Misc
See also notes on:
 SMT
 prolog
 datalog
TPTP
TPTP Thousands of Problems for Theorem Provers is an incredible resource Quick Guide
A couple different input formats. As a human, tff is probably the best. Typed first order formula. cnf is painful, fof is untyped and you’re likely to screw it up imo. tff offers built in ints, which is cool.
TPTP in latex Axiom List Highlights:
 PUZ  puzzles
 GEO  geometry
 GRP  group theory
 CAT  category theory
 SET  set theory
 NUM  number stuff robinson arithmetic
 TOP
 DAT  datatypes
Automated reasoning book
 puzzles
 circuit design (other sythesis problems?)
 program verification
Using for higher order or typed systems
I took a big dump of the axioms because they are hard to peruse. You can find them in my notes. They are very interesting.
Methodology
I find I am often making inconsistent theories because I am trying to be too cute and avoid writing burdensome and inefficient side conditions. A neat thing though is that
Sanity checks:
 Make sure your axioms can’t derive a contradiction. Run vampire or eprover and it should hopefully hang or produce a model
 Make sure there are at least two elements that haven’t collapsed. I find I tend to make theories that collapse
 If you have a simpler seeming axiom than the one that feels to most trustworthy, write them both and ask for equivalence to be proven. If it works, then you can be a little more sure that your simpler axiom is correct.
Puzzles
Math
Groups Lattices kleene algebra, kat
Categories Set theory https://en.wikipedia.org/wiki/List_of_set_identities_and_relation Geometry
antiderivatives
thf(manitype, type, mani : $tType). % manifold
thf(consttype, type, const : $real > mani > $real ).
thf(xtype, type, x : mani > $real ). % coordinate function
thf(ytype, type, y : mani > $real ). % coordinate function
thf(rtype, type, r : mani > $real ). % coordinate function
thf(plustype, type, plus : (mani > $real) > (mani > $real) > mani > $real ). % coordinate function
thf(plusaxioms,axiom, (plus @ X @ Y) = (plus @ Y @ X)).
thf(consttype, type, const : $real > mani > $real ).
%thf(dtype, type, d : (mani > $real) > ).
thf(sintype, type, sin : (mani > $real) > mani > $real).
%thf(powtype,type, > )
thf
^ [X] : X
is a lambda
[a,b,c]
is a built in tuple.
$i
is a universe of individuals
$o
is bools $true
$false
$real
$int
ATP as a Logical Framework
I am used to in the prolog and datalog context to consider the clauses not as classical logical clauses, but instead a description of inference rules. This is the attitude in Miller & Nadathur and The Logic of Logic Programming
It seems to me that there is nothing preventing this interpretation for ATP as well. There are a numbr of axiom sets in the TPTP library that have thsi flavor
~ a
is the same as
a

This is how we express a goal.
~a  b is
a

b
~a  ~c  b
is
a c

b
Putting together clauses (resolution) is interpreted as putting together inference rules to make proof fragments.
% finite sets either by AC axioms or some primitive
cnf(and_comm, axiom, and(A,B) = and(B,A)).
cnf(and_assoc, axiom, and(A,and(B,C)) = and(and(A,B),C)).
cnf(not_intro ,axiom, ~ turnstile(and(C, not(A)), B)  turnstile(C , and(A,B)).
Multiple consequence logic. Smiley https://en.wikipedia.org/wiki/Multipleconclusion_logic
Symbolic Execution
Wos book chapter
Lambda
thf(easymode, conjecture, ?[P : $i > $i] : ((P @ X) = X)).
echo '
thf(f_type, type, f : $i > $i > $i).
thf(f_type, type, g : $i > $i > $i).
% thf(g_permutes_f, axiom, ![X:$i, Y:$i]:((f @ X @ Y) = (g @ Y @ X))).
thf(conj, conjecture, ?[G: $i > $i > $i]: (![X:$i, Y:$i]: ( (f @ X @ Y) = (G @ Y @ X)) ) ).
' > /tmp/example.p
eproverho auto proofobject /tmp/example.p
echo '
thf(unifythis, conjecture, ?[P : $i > $i] : (![X : $i]: ((P @ X) = X))).
' > /tmp/example.p
eproverho auto /tmp/example.p conjecturesarequestions #fails wth GaveUp
eproverho auto /tmp/example.p printstrategy > /tmp/strategy # succeeds
eproverho auto /tmp/example.p conjecturesarequestions parsestrategy=/tmp/strategy #succeeds
echo '
%re
thf(f_type, type, f : $i > $i > $i ).
thf(unifythis, conjecture, ?[P : $i > $i > $i] : (![X : $i, Y : $i]: ((P @ X @ Y) = (f @ Y @ X)))).
' > /tmp/example.p
eproverho auto /tmp/example.p conjecturesarequestions #fails wth GaveUp
eproverho auto /tmp/example.p printstrategy > /tmp/strategy # succeeds
eproverho auto /tmp/example.p conjecturesarequestions #parsestrategy=/tmp/strategy #succeeds
echo '
%re
#thf(f_type, type, x : $i).
thf(easymode, conjecture, ?[P : $i > $i] : (![X : $i]: ((P @ X) = X))).
%thf(easymode, conjecture, ?[P : $i > $i] :((P @ x) = x)).
' > /tmp/example.p
eproverho auto /tmp/example.p conjecturesareequations #fails
eproverho auto /tmp/example.p printstrategy > /tmp/strategy
eproverho auto /tmp/example.p conjecturesarequestions parsestrategy=/tmp/strategy
# printstrategy #conjecturesarequestions
 eproverho –auto /tmp/example.p –proofobject
Conjecturesasquestions is segfaulting. Ok fixed.
Hmm. Why is auto
necessary to make this work? Kind of odd behavior even if in the readme
Lambda lifting
echo '
thf(f_type, type, f : $i > $i ).
thf(problem1, conjecture, ?[G : $i > $i]: (![X: $i]: ((f @ X) = (G @ X)))). ' > /tmp/example.p
eproverho auto /tmp/example.p conjecturesarequestions #proofobject
# This ought to be imposble. Ok Good.
echo '
thf(f_type, type, f : $i > $i ).
thf(problem1, conjecture, ?[G : $i > $i]: (![X: $i, Y:$i]: ((f @ X) = (G @ Y)))). ' > /tmp/example.p
eproverho auto /tmp/example.p proofobject
Structures
In coq or lean we prove somwethign has properties, then we abstract it an use only the properties
thf(monoid_def, axiom, monoid(E, Op) <=> ( ! [X,Y,Z] : (
Op @ (Op @ X @ Y) @ Z = Op @ X @ (Op @ Y @ Z)
& Op @ E @ X = X
& Op @ X @ E = X
))).
Peano
fof(myaxioms, axiom,
nat(z) % unnecessary?
& (nat(X) => nat(s(X)))
& (s(X) = s(Y) => X = Y) % need nat(X) nat(Y) ?
& s(X) != z
% induction is of course the sticky one
% & (((P @ z) & (! [X] : (P @ X => P @ (s(X))))) => P @ Y)
).
Getting Saturated with Induction
ECTS
% don't connect posibly non well formed things
cnf(comp_assoc, axiom, comp(X,comp(Y,Z)) = comp(comp(X,Y),Z)).
cnf(wf_comp, axiom, ~wf(F)  ~wf(G)  dom(F) != cod(G)
 wf(comp(F,G))).
cnf(wf_id, axiom, wf(id(A))).
cnf(comp_id_left, axiom, comp(id(cod(F)),F) = F).
cnf(comp_id_right, axiom, comp(F,id(dom(F))) = F).
cnf(term_final, axiom, cod(F) != unit  cod(G) != unit  dom(F) != dom(G)
 F = G ).
%fof(elem_def, axiom, elem(X,A) <=> ( comp(X,A) ) )
What about doing bash + vampire as a proof system
What about universes?
Set Theory
TPTP has tons of axiom sets for this. But let’s play around
fof(mystuff, axiom,
$true
%~ elem(X,empty)
& ((elem(X,A)  elem(X,B)) <=> elem(X,union(A,B)))
%& ((elem(X,A) & elem(X,B)) <=> elem(X,inter(A,B)))
%& (elem(X,sing(Y)) <=> (X = Y))
%& ( (![X] : (elem(X,A) <=> elem(X,B))) <=> (A = B)) % extensionality
%& ( (![X] : (elem(X,A) => elem(X,B))) <=> sub(A,B))
).
%fof(sub_equal, conjecture, (sub(X,Y) & sub(Y,X)) <=> (X = Y) ).
%fof(union_comm, conjecture, union(A,B) = union(B,A)).
fof(union_assoc, conjecture, union(A,union(B,C)) = union(union(A,B),C)).
Free Logic / Partial Functions
See the category theory CAT003 example in TPTP with comments about paper by Scott Identity and Existence in Intuitionist Logic Avigad book Free logic article
We don’t want it necessarily to assume our function symbols are total. How do we model this? We could switch t a relational character. Functions are so gosh darn nice though.
Query Containment
Queries are first order logical statements with perhaps some free variables. They ae evaluated (model checked) with respect to particular finite models. Asking if one statement implies another in all models is semantic entailment.
Because 
and =
are the same thing here (? Really we are relying on soundness), We can write query containment as a simple theorem proving question
fof(q1_def, axiom, q1(X) <=> (r(X,Y) & r(Y,X))). % just implication or biimplication?
fof(q2_def, axiom, q2(X) <=> r(X,Y)).
fof(contain, conjecture,
q1(X) => q2(Q)
).
This also implies a method for solving CSPs.
% or really the full clark completion? Yea. I almost certainly do need it.
fof(k3_edges, axiom, k3edge(a,b) & k3edge(b,c) & k3edge(c,a) & k3edge(b,a) & k3edge(c,b) & k3edge(a,c)
& ~k3edge(a,a) & ~k3edge(b,b) & ~k3edge(c,c)
).
fof(mygraph, axiom, edge(1,2)).
fof(verts, axiom, vert(V) <=> (edge(V,X))  edge(X,V)).
fof(color3 , conjecture, edge(X,Y) => k3(color(X),color(Y)))
hhmmm.
Systems
 Vampire
 E Prover https://wwwlehre.dhbwstuttgart.de/~sschulz/E/E.html
 Zipperposition
 https://github.com/tammet/gkc on an in memory database
 Twee: An Equational Theorem Prover
Vampire
FirstOrder Theorem Proving and VAMPIRE vampire tutorial
% https://www.tptp.org/TPTP/QuickGuide/Problems.html
%
%All (hu)men are created equal. John is a human. John got an F grade.
%There is someone (a human) who got an A grade. An A grade is not
%equal to an F grade. Grades are not human. Therefore there is a
%human other than John.
fof(all_created_equal,axiom,(
! [H1,H2] :
( ( human(H1)
& human(H2) )
=> created_equal(H1,H2) ) )).
fof(john,axiom,(
human(john) )).
fof(john_failed,axiom,(
grade(john) = f )).
fof(someone_got_an_a,axiom,(
? [H] :
( human(H)
& grade(H) = a ) )).
fof(distinct_grades,axiom,(
a != f )).
fof(grades_not_human,axiom,(
! [G] : ~ human(grade(G)) )).
fof(someone_not_john,conjecture,(
? [H] :
( human(H)
& H != john ) )).
%
% a silly axiomatization of add and theorem.
% using typed formula
tff(num_type,type,
num: $tType ).
tff(add_type,type,
add: ( num * num ) > num ).
tff(zero_type,type,
zero: num ).
tff(add_zero_axiom,axiom,
! [X: num] : add(X, zero) = X ).
tff(add_comm_axiom,axiom,
! [X: num, Y : num] : add(X, Y) = add(Y,X) ).
tff(mytheorem, conjecture, ? [X : num] : add(zero, X) = X).
% https://www.tptp.org/cgibin/SeeTPTP?Category=Problems&Domain=DAT&File=DAT001=1.p
tff(list_type,type,
list: $tType ).
tff(nil_type,type,
nil: list ).
tff(mycons_type,type,
mycons: ( $int * list ) > list ).
tff(sorted_type,type,
sorted: list > $o ).
tff(empty_is_sorted,axiom,
sorted(nil) ).
tff(single_is_sorted,axiom,
! [X: $int] : sorted(mycons(X,nil)) ).
tff(recursive_sort,axiom,
! [X: $int,Y: $int,R: list] :
( ( $less(X,Y)
& sorted(mycons(Y,R)) )
=> sorted(mycons(X,mycons(Y,R))) ) ).
tff(check_list,conjecture,
sorted(mycons(1,mycons(2,mycons(4,mycons(7,mycons(100,nil)))))) ).
Array axioms. Also axioms for int collections, int map, heaps. They all boil to pretty similar stuff though
% https://www.tptp.org/cgibin/SeeTPTP?Category=Axioms&File=DAT001=0.ax
tff(array_type,type,
array: $tType ).
tff(read_type,type,
read: ( array * $int ) > $int ).
tff(write_type,type,
write: ( array * $int * $int ) > array ).
tff(ax1,axiom,
! [U: array,V: $int,W: $int] : ( read(write(U,V,W),V) = W ) ).
tff(ax2,axiom,
! [X: array,Y: $int,Z: $int,X1: $int] :
( ( Y = Z )
 ( read(write(X,Y,X1),Z) = read(X,Z) ) ) ).
% https://www.tptp.org/cgibin/SeeTPTP?Category=Axioms&File=DAT001=0.ax
tff(array_type,type,
array: $tType ).
tff(read_type,type,
read: ( array * $int ) > $int ).
tff(write_type,type,
write: ( array * $int * $int ) > array ).
tff(ax1,axiom,
! [U: array,V: $int,W: $int] : ( read(write(U,V,W),V) = W ) ).
tff(ax2,axiom,
! [X: array,Y: $int,Z: $int,X1: $int] :
( ( Y = Z )
 ( read(write(X,Y,X1),Z) = read(X,Z) ) ) ).
fof(ground, axiom,
edge(1,2) & edge(2,3)
).
%fof(path1, axiom,
% ![X,Y]: (edge(X,Y) => path(X,Y))
%).
%fof(path2, axiom,
% ![X,Y,Z]: ((edge(X,Y) & path(Y,Z)) => path(X,Z))
%).
fof(clark, axiom,
![X,Z]: (((?[Y]: (edge(X,Y) & path(Y,Z)))  edge(X,Z)) <=> path(X,Z))
).
fof(myquery, conjecture,
?[X,Y]: path(X,Y)
%path(1,2)
).
vampire av off –question_answering answer_literal
fof(a,axiom,prover(vampire)).
fof(a,axiom,prover(e)).
fof(a,axiom,tutorial(vampire)).
fof(a,axiom,tutorial(probabilistic)).
fof(a,conjecture,?[X]: (prover(X) & tutorial(X))).
sos
inference restrictions
unit_resulting_resolution
echo "
fof(ground, axiom,
edge(a,b) & edge(b,c)
).
fof(path1, axiom,
![X,Y]: (edge(X,Y) => path(X,Y))
).
fof(path2, axiom,
![X,Y,Z]: ((edge(X,Y) & path(Y,Z)) => path(X,Z))
).
"  vampire unit_resulting_resolution on
Hmm. Vampire with the option or not. Not really sure what to take away from that. It might be recogzninig a datalog fragment If I wanted to use this like an egraph, I can’t look inside the equality. It’s entirely unobseravle. Maybe I could use the reflection trick.
E prover
enormalizer is an interesting sounding program. Give it a pile of unit equalities and it will normalize with respect to thm EPR grounder to DIMACS The e calculus is a bit puzzling. I haven’t seen the analog for vampire
2.6 manual It’s also in the github repo if you make doc
I like how –answer mode works a little better for e.
Database printing feature S. Doesn’t print stuff I would expect though? Kind of prints everything by default right? Early stopping conditions clause size
eprover help  less
watchlist
 “constructive” proofs that aren’t seeded by refuation
training  you can train it if you have a database of indicative theorems. This might be useful if you have a sequence of increasingly hard theorems, or if you are making a tool that spits out formula.
S
print saturated clause set
W
literaeelection stretagory NoGeneration will inhibit all generating instances “Each of the strategies that do actually select negative literals has a corresponding counterpart starting with P that additionally allows paramodulation into maximal positive literals”
echo "
fof(ground, axiom,
edge(a,b) & edge(b,c)
).
fof(path1, axiom,
![X,Y]: (edge(X,Y) => path(X,Y))
).
fof(path2, axiom,
![X,Y,Z]: ((edge(X,Y) & path(Y,Z)) => path(X,Z))
).
"  eprover literalselectionstrategy=SelectNegativeLiterals
generatedlimit=100
Ok this basically did what i wanted. I’m not sure what it is though?
“The most natural clause representation for E is probably a literal disjunction: a=$true;b!=$true;c!=$true.”
Prover9
Prover9 and Mace4 Prover9 is intriguing. It seems to have interaction modalities that other provers don’t Mace proverx a web gui variant
Some examples I didn’t write:
echo "% Prove that a group in which all elements have order 2 is commutative.
assign(max_seconds, 60).
formulas(assumptions).
% group axioms
(x * y) * z = x * (y * z). % associativity
1 * x = x. % left identity
x * 1 = x. % right identity
x' * x = 1. % lef inverse
x * x' = 1. % right inverse
% special assumption
x * x = 1. % all elements have order 2
end_of_list.
formulas(goals).
x * y = y * x.
end_of_list.
"  prover9
if(Prover9).
assign(order, kbo).
assign(max_weight, 25).
end_if.
formulas(sos).
% lattice theory
x v y = y v x.
(x v y) v z = x v (y v z).
x ^ y = y ^ x.
(x ^ y) ^ z = x^ (y ^ z).
x ^ (x v y) = x.
x v (x ^ y) = x.
end_of_list.
formulas(sos).
(x ^ y) v (x ^ z) = x ^ ((y ^ (x v z)) v (z ^ (x v y))) # label(H82).
end_of_list.
formulas(goals).
x ^ (y v (x ^ z)) = x ^ (y v (z ^ ((x ^ (y v z)) v (y ^ z)))) # label(H2).
end_of_list.
assign(order, kbo). % The default (lpo) al works, but it takes longer.
formulas(assumptions).
% Prover9 should produce a proof in a few seconds.
% combinators B and W
a(a(a(B,x),y),z) = a(x,a(y,z)) # label(B).
a(a(W,x),y) = a(a(x,y),y) # label(W).
end_of_list.
formulas(goals).
% existence of a fixed point combinator
exists Q all x (a(Q,x) = a(x,a(Q,x))) # label(fixed_point_combinator).
end_of_list.
% Here is a different way of specifying the goal, which tells us
% what the fixed point combinator is. We use an answer attribute.
% Unfortunately, answer attributes are not allowed on nonclausal
% (e.g., goal) formulas, so we deny the goal and state it as an assumption.
% Note that this introduces the Skolem function f.
%
% formulas(assumptions).
% a(x,f(x)) != a(f(x),a(x,f(x))) # answer(x).
% end_of_list.
Otter
https://www.cs.unm.edu/~mccune/otter/ otter lambda  dumping lambda terms in otter? http://www.michaelbeeson.com/research/otterlambda/ Otter seemed to offer more control over the resolution process Prover9 is the succssor to otter
otter manual “Although OTTER has an autonomous mode, most work with OTTER involves interaction with the user”
LeanTAP and ilk
See prolog some Build Your Own FirstOrder Prover https://www.philipzucker.com/javascriptautomatedproving/
PyRes
 https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7324010/ Teaching Automated Theorem Proving by Example: PyRes 1.2
 pyressimple is a minimal system for clausal logic, pyrescnf adds heuristics, indexing, and subsumption, and pyresfof
# atomic formula first. Ground is basically the same.
# sets are unhashable, so are lists
#print({[], []})
# One canonical form is sorted, deduped pos,neg lists for clauses
def clause(pos,neg):
return (tuple(sorted(set(pos))), tuple(sorted(set(neg))))
print(clause(["a","a"], ["c"]))
print(clause(["foo(a)","bar(a)"], ["c"]))
# we could also put a wrapper around set that does have a hash defined
def resolve(C1,C2):
C1[0].diff(C2[1])
C2[0].diff(C1[1])
if len(C1[0].intersect(C2[1])) > 0:
processed = set()
unprocessed = []
while len(unprocessed) > 0:
C = unprocessed.pop()
for C1 in processed:
resolve(C1,C)
# terms are sexp style lists
# ["f", ["a"], ["g", "b"]]
A sqlized givenclause loop
unproc = []
proc = sqlite3.connect(":memory:") # store processed clauses in DB.
while len(unproc) > 0:
C.pop(unproc)
sql = query(C)
unproc.append(filter(cur.fetchall(), lambda: do_some_filtering))
cur.execute("INSERT INTO", C)
Ground Subsumption queyr on clauses. Find all sets that have C as subset
CREATE Table lit (clause INTEGER, lit STRING);  UNIQUE (clause, lit) gives redundant lit deletion
 find all clauses c such it contains literal a,b,c.
SELECT DISTINCT clause from lit a, lit b, lit c where a.clause = b.clause and a.clause = c.clause and a.lit = ? and b.lit = ? and c.lit = ?
Find all sets that have C as superset
SELECT DISTINCT clause from lit a
group by a.clause
HAVING COUNT(CASE WHEN lit = ? THEN 1 END) + COUNT(CASE WHEN lit = ? THEN 1 END) + COUNT(CASE WHEN lit = ? THEN 1 END) = count(*);
count(case when lit != ? or lit != ? or lit != ? then 1 end) = 0
count(*) <= 3  would this help or hurt? redundant info
and
min(case when lit = ? then 1 when lit = ? when else 0 ) = 1
t1 = "fah0"
t2 = "f01"
i1 = 0
i2 = 0
while i1 < len(t1) and i2 < len(t2):
c1 = t1[i1]
c2 = t2[i2]
if t2
grammar = '''
E : F  G  Var  A
F : "f" E E
A : "a"
Var : NUMBER
'''
grammar = '''
Term : CNAME  CNAME "(" ("," Term)* ")"  Var
'''
class Unify(Transformer):
env = {}
def Var(self, v):
if v in env:
def term
Big question is, what is the representation of formulas, literals, clauses.
 Strings
 Json
 Relational Terms / hashconsed
 Feature vectors.
Zipperposition
logtk. Huh. LPO as a constraint solving problem https://sneeuwballen.github.io/zipperposition/2.0/logtk/Logtk_solving/index.html
#use "topfind";;
#require "logtk";;
print_endline "hello world";;
open Logtk
(* https://github.com/sneeuwballen/zipperposition/blob/master/tests/testTerm.ml *)
module T = Term
let f_ = ID.make "f"
let g_ = ID.make "g"
let ty = Type.term
let ty_t = Term.of_ty ty
let prop = Type.prop
let f_fun = (T.const ~ty:Type.([ty;ty] ==> ty) f_)
let f x y = T.app f_fun [x; y]
let prec = Precedence.default [f_;g_]
(*let ord = Logtk.Ordering.lambda_kbo prec *)
let names = Ordering.names ()
let () = List.iter (fun name > print_endline name) names
Datalog vs ATP
What makes an ATP that different from a datalog? Both are saturating. If I could limit of prune clauses of size > N, that might emulate a datalog. Or perhaps protect rulerule resolution from happening.
The given clause algorithm has some flavor of seminaive. Datalog focuss on unit clauses Not at all clear how to do extraction on a paramodulated database.
Given that ATP subsumes in some sense both prolog and datalog, what does it say about Magic Set?
Extraction from ATP. The equality is invisible. The copying trick?
Prolog vs ATP
Set of support strategy with horn clauses in passive set, goal in active set, hyperresolution as only inference rule behaves akin to prolog.
What is the difference between E and a PROLOG system?
Prolog =
is unification. ATP =
is rewrite/semantical.
ATP vs ITP
Imandra
I don’t know if this really belongs in this note Imandra is like ACL2 for ocaml I think python interface
import imandra
Strategies
Relationship to focusing http://web4.ensiie.fr/~guillaume.burel/download/LFAT.pdf
Set of Support  Only infer on clauses that trace provenance to user specified set of support.
https://www.doc.ic.ac.uk/~kb/MACTHINGS/SLIDES/2013Notes/7LControl4up13.pdf The Predicate Ordering Syntactic Refinement  order predicates. Only resolve on lowest Locking Refinement  mark each literal in clause and resolve only on lowest one atom ordering
 Resonance Strategy
 Weighting
Methodology
Given clause Discount loop
Unification
 see note on unification Two way matching. Is there a substitution for variables that solves an equation. Yes
Antiunification is an interesting topic. Generalization.
# https://github.com/pythological/unification
from unification import var, unify
x = var("x")
y = var("y")
y1 = var("y") # same y.
print(unify((x,y), (y1,1))) # returns subst dict
Or can use Maude’s unification. Or prolog’s. Or just write it.
Resolution
Put clauses in cnf. Each clause is an \/
of positive and negative atoms.
Take two clauses that have matching (unifiable) positive and negative pieces
Hyperresolution https://www.doc.ic.ac.uk/~kb/MACTHINGS/SLIDES/8LHyper4up.pdf You are seeking clauses of only positive literals. Only use a “nuecleii” if it covers all of the negative literals.
URresolution  unitresulting resolution. Only perform resultion if it results in nw unit literal (all other chunks line up). UR is essentially datalog stye resolution. It does however allow universals in the unit facts.
SLD resolution is ATP view of prolog.
Factoring
# Ground resolution
from typing import Any
Form = Any
Lit = Tuple[bool,Form]
Clause = Set[Lit]
def factor(c, i1, i2):
(pos1, fm1) = c1[i1]
(pos2, fm2) = c2[i2]
assert pos1 != pos2
assert fm1 == fm2
res = []
for i,x in enumerate(c1)
if i != i1 and i != i2:
res.append(x)
return res
def resolve(c1,i1, c2, i2):
(pos1, fm1) = c1[i1]
(pos2, fm2) = c2[i2]
assert pos1 != pos2
assert fm1 == fm2
res = []
for i,x in enumerate(c1)
if i != i1:
res.append(x)
for i,x in enumerate(c2)
if i != i2:
res.append(x)
return sorted(res)
processed = []
unprocessed = []
def resolve_cand(lit):
lit2 = (not lit[0], lit)
for c in processed:
if lit2 in c:
while len(unprocessed) != 0:
c = unprocessed.pop()
for lit in c:
resolve_cand(lit)
cnew = resolve(c,i,c, i2)
if cnew not in processed:
unprocessed.append(cnew)
Index = Dict[Lit,Set[Clause]]
Subsumption
Cleaning out the database.
given C(X) , C(a) is redundant (subsumed). You can remove it from clause database. A question is how to do this quickly. See Term indexing.
https://www.doc.ic.ac.uk/~kb/MACTHINGS/SLIDES/2013Notes/6LSub4up13.pdf https://www.cs.cmu.edu/~fp/courses/99atp/lectures/lecture20.html
encoding subusmption to SAT https://fmcad.org/FMCAD22/presentations/08%20%20SAT%20and%20SMT%202/01_rath.pdf
Narrowing
see term rewriting
Paramodulation
paramodulation is unification based equational substitution
Paramodulation is dealing with equality pieces in clauses. http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.34.9958&rep=rep1&type=pdf
Demodulation
rewrite rules basically? destructively simplify terms using them Positive literals can be marked or inferred as demodulators (what we ordinary think of as rewrite rules) By having both paramodulation and demodulation exist, the system has both destructive and conservative rules.
Superposition
https://en.wikipedia.org/wiki/Superposition_calculus
ntroduction to Superposition calculus  Cruanes slides
New results on rewritebased satisfiability procedures
Term orderings  see term rewriting
Implementation of Saturating Theorem Provers
Superposition 25 http://www.eprover.org/EVENTS/Superposition25/TutorialSP_ho.pdf
superposition can be used instead of resolution by encoding predicates as functions to true
If I run superposition on unit positive clauses, is it performing completion? Completion of guarded rewrite systems?
The discussion of the encoding of t = s is a bit goofy. Yes, =
is commutative. In that sense in is reasoonable to use sets. Could the opposite convention be used? This is kind of like the settheoretic convention of (a,b) === { {a}, {a,b} __ }
(stupid liquid formatting error) which is pretty bizarre too
t = s === { __ {t}, {s} __ }
t != s === { __ {t,s} __ }
Multiset orderings
Literal Selection
Ordered resolution  order on literals, only resolve on biggest one (you want to get rid of big stuff)
Term Indexing
Triemaps that match SPJ and Graf https://www.youtube.com/watch?v=cT8G6FS2v94&ab_channel=Konfy
type expr = Var of string  App of expr * expr
type 'a exprmap = {var : 'a String.Map.t; app : 'a exprmap exprmap } (* I thing if we play that nested data structure stuff we're gonna have a bad time in ocaml*)
See Automated reasoning handbook chapter 18 https://www.cs.cmu.edu/~fp/courses/atp/lectures/22indexing.html towards efficient subsumption  Tammet Give reasoning a trie Indexes are pretty good for serialized structures. You can serialize a term/tree by . Perfect indexing vs approximate indexing. You don’t necessarily need to index only the terms you need. YOu can iterate over the returned bits and just toss out the stuff you didn’t want. Depends how expensive perfect vs imperfect is
Indexing has different kinds of queries. Is the database ground or not?
 Variants
 Unifiers
 Forward Subsumption
 Backwards subsumption You may want multiterm indexing
Path Indexing
most suitable for backward subsumption) Consider paths from root to leaf of tree. Can put this in a trie. Look at all paths in a query term of interest and take set intersection from path index trie.
Generalization? Consider just paths through a graph? f(a,b,c), g(a,d,c), … . Up down and around. Kind of reminds me of code2vec
Discrimination Trees
most suitable for unit forward subsumption
A depth first traversal of the whole term
Substitution trees
Feature Vectors
Simple and Efficient Clause Subsumption with Feature Vector Indexing
Fingerprint Indexing for Paramodulation and Rewriting
You can make summary data on terms that is monotonic with respect to instantation.
count and max depth appearance of symbols. A generalization of seperating terms out by their head symbol Imperfect indexing is useful. It does mean you may have to implement algorithms more than once.
Theories
Inductiion Superposition with Structural Induction Datatypes Superposition with Datatypes and Codatatypes Arrays Arith Beagle – A Hierarchic Superposition Theorem Prover
Higher Order
Applicative encoding. Turn f(x,y)
into app(app(f,x),y)
. Wasteful and inefficint but it can work. Built in appreciation of higher order structure (currying basically?) is better
Higher order lambda free.
HORPO  term orderings that appreciate the applicative structure
superposition for lambda free higher order
Mechanical Mathematicians A new generation of automatic theorem provers eliminate bugs in software and mathematics
Differentiation? antiderivative search
Inside higher order systems Meson hammers blast FirstOrder Proof Tactics in HigherOrder Logic Theorem Provers  Hurd Metis
Misc
Uwe Waldemann  automated reasoning courses
OrderingBased Strategies for Hor n Clauses*  Dershowitz Equational horn clause. positive is larger than negative in literal selection
33 Basic Test Problems: A Practical Evaluation of Some Paramodulation Strategies
Set of Support, Demodulation, Paramodulation: A Historical Perspective pfenning book
loveland book fitting book theorem proving in otter
wos summary https://ininet.org/automatedreasoningandresolution.html
http://wp.doc.ic.ac.uk/kb/teaching/ autmated reasoning course krysia
Set of Support prio
 https://logictools.org/ neat online ATP interface

TPTP
 Sledgehammer
Resolution is bottom up, tableau is top down?
Automated Deduction in Equational Logic and Cubic Curves
 Idea: Convert resolution proof to bus proofs tree. Is this even possible or desirable?
Schulz teaching automated theorem proving polymorphic vampire
An Impossible Asylum  ATP checking of Smullyan puzzle found hypotheses inconsistent
Phillips & Stanovsky https://www2.karlin.mff.cuni.cz/~stanovsk/math/slides_esarm.pdf loop theory and non associative lagerbas https://www2.karlin.mff.cuni.cz/~stanovsk/math/slides_lpar08.pdf
Searching for a Fixed Point Combinators by Using Automated Theorem Proving: A Preliminary Report
Challenge Problems Focusing on Equality and Combinatory Logic: Evaluating Automated TheoremProving Programs
tptp bibiography. It’s insane how much work is here
geometric database horn clauses.
Waldmeister and Twee  UEQ
REDUCING HIGHERORDER THEOREM PROVING TO A SEQUENCE OF SAT PROBLEMS
Dedam: A Kernel of Data Structures and Algorithms for Automated Deduction with Equality Clauses
efficient full higher order unification zipperposition
Thesis on Implementation of HigherOrder Superposition
auto2 interesting system that combines egraphs and sturation proving https://github.com/bzhan/auto2 he alos mentions gowers as influence Coming to Terms with Quantified Reasoning algerbaic datatypes require an infinite number of acyclicity axioms.
https://www.ps.unisaarland.de/Publications/documents/Treinen_tacs91.pdf FOL + datatypes is more powerful than just FOL.
from pysmt.shortcuts import get_env
from pysmt.logics import LOGICS
from pysmt.shortcuts import Symbol, get_env, Solver
env = get_env().factory.add_generic_solver("vampire", ["/home/philip/.local/bin/vampire", "input_syntax", "smtlib2"], LOGICS)
print("opening")
with Solver(name="vampire", logic="QF_UFLRA") as s:
print("starting")
print(s.is_sat(Symbol("x"))) # True
from z3 import *
s = Solver()
x = Bool("x")
s.add(And(x, Not(x)))
#s.add(x)
s.check()
print(s.to_smt2())
import tempfile
import subprocess
with tempfile.NamedTemporaryFile(suffix=".smt2") as fp:
fp.write(s.to_smt2().encode() + b"(getmodel)")
fp.flush()
res = subprocess.run(["/home/philip/.local/bin/vampire", fp.name], capture_output=True)
print(res.stdout.decode())