|
 
|
[BC13] Detection of First Order Axiomatic Theories
Conférence Internationale avec comité de lecture : Frontiers of Combining Systems 2013, September 2013, Vol. 8152, pp.229-244, Series LNCS, Nancy, France, (DOI: 10.1007/978-3-642-40885-4_16)Mots clés: Theories, Datalog, Axiom, Lemma, Signature, Superposition
Résumé:
Automated theorem provers for first-order logic with equality have
become very powerful and useful, thanks to both advanced calculi —
such as superposition and its refinements — and mature implementation
techniques. Nevertheless, dealing with some axiomatic theories remains
a challenge because it gives rise to a search space explosion. Most
attempts to deal with this problem have focused on specific theories,
like AC (associative commutative symbols) or ACU (AC with neutral
element). Even detecting the presence of a theory in a problem is
generally solved in an ad-hoc fashion. We present here a generic way of
describing and recognizing axiomatic theories in clausal form
first-order logic with equality. Subsequently, we show some use cases
for it, including a redundancy criterion that can be applied to some
equational theories, extending some work that has been done by Avenhaus,
Hillenbrand and Löchner.
Equipe:
sys
Collaboration:
Ecole Polytechnique
BibTeX
| @inproceedings { | |||
| BC13, | |||
| title | = | "{Detection of First Order Axiomatic Theories}", | |
| author | = | " G. Burel and S. Cruanes ", | |
| booktitle | = | "{Frontiers of Combining Systems 2013}", | |
| year | = | 2013, | |
| month | = | "September", | |
| series | = | "LNCS", | |
| volume | = | 8152, | |
| pages | = | "229-244", | |
| address | = | "Nancy, France", | |
| doi | = | "10.1007/978-3-642-40885-4_16", | |
| } | |||
