Detection of First Order Axiomatic Theories

Guillaume Burel 1, 2 Simon Cruanes 1
2 CPR
CEDRIC - Centre d'Etude et De Recherche en Informatique du Cnam
Abstract : 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
Type de document :
Communication dans un congrès
Pascal Fontaine and Christophe Ringeissen and Renate A. Schmidt. FroCoS - 9th International Symposium on Frontiers of Combining Systems - 2013, Sep 2013, Nancy, France. Springer, 8152, pp.229-244, 2013, Frontiers of Combining Systems. 〈http://link.springer.com/chapter/10.1007/978-3-642-40885-4_16〉. 〈10.1007/978-3-642-40885-4_16〉
Liste complète des métadonnées

Littérature citée [14 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-00919759
Contributeur : Simon Cruanes <>
Soumis le : mardi 17 décembre 2013 - 11:51:22
Dernière modification le : mardi 17 avril 2018 - 11:27:59
Document(s) archivé(s) le : lundi 17 mars 2014 - 22:45:45

Fichier

theory_detection_free.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Guillaume Burel, Simon Cruanes. Detection of First Order Axiomatic Theories. Pascal Fontaine and Christophe Ringeissen and Renate A. Schmidt. FroCoS - 9th International Symposium on Frontiers of Combining Systems - 2013, Sep 2013, Nancy, France. Springer, 8152, pp.229-244, 2013, Frontiers of Combining Systems. 〈http://link.springer.com/chapter/10.1007/978-3-642-40885-4_16〉. 〈10.1007/978-3-642-40885-4_16〉. 〈hal-00919759〉

Partager

Métriques

Consultations de la notice

178

Téléchargements de fichiers

102