Guillaume BUREL's Homepage (Guillaume Burel's photo)

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:

References

[1] Guillaume Burel. 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.