Autotheo
In [1] we show how to transform any first-order theory into a rewriting system that can be used in deduction modulo. We then conduct an experiment to compare several ways of orienting set of axioms into such rewriting systems.
This page provides the following material:
- The autotheo program automatically transforms axioms from
a TPTP problem into a rewriting system that can be used
by iProver modulo. It takes
as input a TPTP file, extracts the formulas whose TPTP role is
axiom, and translates them into a rewriting system using one of the
following techniques:
- ClausalAll: The set of axioms is put in clausal normal form, and a rewriting rule is produced for each literal of the resulting clauses.
- Sat: The set of axioms is saturated using E, then a rewriting rule is produced for each selected literal of the resulting clauses.
- Id: Returns the set of axioms unchanged.
- Nil: Drop out the set of axioms.
- Presat(H): The set of axioms is saturated using E until a certain amount of clauses have been processed (1000 by default). These processed clauses are transformed into a rewriting system restricted to the selected literals as in Sat. The unprocessed clauses generated during the saturation are transformed using the technique H.
- Equiv(H): According to the shape of the axiom, a rewriting rule is produced; axioms that did not fit these patterns are transformed using the technique H.
tar xvzf autotheo-1.0.tar.gz
Change directorycd autotheo-1.0/src
Make sure you have OCaml installed or install it. Then compile autotheo:make
That's it. To get a list of available options, type./autotheo --help
autotheo takes as input a TPTP file and prints on the standard output the resulting TPTP file that can be used by iProver modulo, containing both the rewriting system and the other (non-axiom) formulas of the original problem. Note that the input format of iProver modulo assumes that rewriting rules are given as cnf formulas whose role is axiom: they are the one-way clauses corresponding to the rules, with the selected literal in first position. - The detailed results of the experiment of [1] are transcribed
in this spreadsheet file
(PDF version).
Files generated by autotheo on the problems selected in last CASC can be found in this archive (90MB).
References
[1] . From axioms to rewriting rules. Submitted. .pdfAbstract Deduction modulo is a generic framework to describe proofs in a theory better than using raw axioms. This is done by presenting the theory through a congruence over propositions that is most often defined by means of rules rewriting terms and propositions. It has been shown that such representations of theories actually improves automated proof search. In this paper, we positively answer the theoretical question whether all first-order theories can be represented by such rewriting systems, while preserving a crucial proof-theoretical property, namely cut admissibility, equivalent to the completeness of proof search. We also perform experiments to compare several techniques to orient axioms into rewriting systems, some of them being complete, some being based on heuristics.