On the practical value of different definitional translations to normal form. In this paper, we compare different normal form translations from a practical point of view. The usual translation of a closed first-order formula to a disjunctive normal form has severe drawbacks, namely the disruption of the formula’s structure and an exponential worst case complexity. In contrast, definitional translations avoid these drawbacks by introducing some additional new predicates yielding a moderate increase of the length of the normal form. In implementations, the standard translation is preferred, possibly because the theorem prover has to cope with some additional redundancy introduced by the new predicates. We show that definitional translations can excellently compete with the usual translation by providing run-time measurements with our theorem prover KoMeT. Moreover, for some problems like the halting problem, proofs can only be obtained in reasonable time if definitional translations are used.

References in zbMATH (referenced in 13 articles , 1 standard article )

Showing results 1 to 13 of 13.
Sorted by year (citations)

  1. Schuppan, Viktor: Towards a notion of unsatisfiable and unrealizable cores for LTL (2012)
  2. Brandt, Christoph; Otten, Jens; Kreitz, Christoph; Bibel, Wolfgang: Specifying and verifying organizational security properties in first-order logic (2010)
  3. Egly, Uwe; Seidl, Martina; Woltran, Stefan: A solver for QBFs in negation normal form (2009)
  4. Otten, Jens; Bibel, Wolfgang: IeanCOP: lean connection-based theorem proving (2003)
  5. Caferra, Ricardo; Peltier, Nicolas: Combining enumeration and deductive techniques in order to increase the class of constructible infinite models (2000)
  6. Egly, Uwe; Rath, Thomas: Practically useful variants of definitional translations to normal form (2000)
  7. Kreitz, Christoph; Schmitt, Stephan: A uniform procedure for converting matrix proofs into sequent-style systems (2000)
  8. Schaub, Torsten; Brüning, Stefan: Prolog technology for default reasoning: proof theory and compilation techniques (1998)
  9. Dahn, B. I.; Gehne, J.; Honigmann, Th.; Wolf, A.: Integration of automated and interactive theorem proving in ILF (1997)
  10. Wolf, Andreas; Schumann, Johann: ILF-SETHEO: processing model elimination proofs for natural language output (1997)
  11. Egly, Uwe; Rath, Thomas: On the practical value of different definitional translations to normal form (1996)
  12. Otten, Jens; Kreitz, Christoph: T-string unification: unifying prefixes in non-classical proof methods (1996)
  13. Schmitt, Stephan; Kreitz, Christoph: Converting non-classical matrix proofs into sequent-style systems (1996)