2 Theoretical Foundations
The h1 prover is based on ordered resolution with selection, and
є-splitting. See the
paper
[Gou05] for a spoonful of proofs and complexity classes.
See [GL06b] for further detailed information on how h1 works, with a focus on three of the most important optimizations
used in h1: naive static soft typing, deep abbreviation, and
full definition subsumption. Here is the submitted
paper.
You can use h1 and h1mc to produce automatic proofs by
induction of invariants. The technique is a variant of inductionless
induction, a.k.a., proof by consistency. If you don't mind reading
French, read the
paper
[GL04]. For those of you who don't speak French (shame on
you!), the title means “Once you failed finding a proof, how do you
explain this to a proof assistant?”.
A much better, more accurate paper, in English, and
with many experimental evidence.
The algorithm behind the linauto Presburger to deterministic
automaton converter is expounded in [BC96].