Computing Tiny Clause Normal Forms

Noran Azmy 1 Christoph Weidenbach 2, 3
1 Automation of Logic
MPII - Max-Planck-Institut für Informatik
3 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
Abstract : Automated reasoning systems which build on resolution or superposition typically operate on formulas in clause normal form (CNF). It is well-known that standard CNF translation of a first-order formula may result in an exponential number of clauses. In order to prevent this effect, renaming techniques have been introduced that replace subformulas by atoms over fresh predicates and introduce definitions accordingly. This paper presents generalized renaming. Given a formula and a set of subformulas to be renamed, it is suggested to use one atom to replace all instances of a generalization of a given subformula. A generalized renaming algorithm and an implementation as part of the SPASS theorem prover are described. The new renaming algorithm is faster than the previous one implemented in SPASS. Experiments on the TPTP show that generalized renaming significantly reduces the number of clauses and the average time taken to solve the problems afterward.
Type de document :
Communication dans un congrès
Maria-Paola Bonacina. 24th International Conference on Automated Deduction (CADE-24), Jun 2013, Lake Placid, NY, United States. Springer, 7898, pp.109-125, 2013, Lecture Notes in Computer Science. 〈10.1007/978-3-642-38574-2_7〉
Liste complète des métadonnées

https://hal.inria.fr/hal-00931893
Contributeur : Stephan Merz <>
Soumis le : jeudi 16 janvier 2014 - 09:16:18
Dernière modification le : jeudi 20 septembre 2018 - 07:54:02

Identifiants

Collections

Citation

Noran Azmy, Christoph Weidenbach. Computing Tiny Clause Normal Forms. Maria-Paola Bonacina. 24th International Conference on Automated Deduction (CADE-24), Jun 2013, Lake Placid, NY, United States. Springer, 7898, pp.109-125, 2013, Lecture Notes in Computer Science. 〈10.1007/978-3-642-38574-2_7〉. 〈hal-00931893〉

Partager

Métriques

Consultations de la notice

159