hal-00008804, version 1
Combining proof-search and counter-model construction for deciding Gödel-Dummett logic
18th International Conference on Automated Deduction - CADE 18 2362 (2002) 94-110
Abstract: We present an algorithm for deciding Gödel-Dummett logic. The originality of this algorithm comes from the combination of proof-search in sequent calculus, which reduces a sequent to a set of pseudo-atomic sequents, and counter-model construction of such pseudo-atomic sequents by a fixpoint computation. From an analysis of this construction, we deduce a new logical rule which provides shorter proofs than the previous rule of G4-LC. We also present a linear implementation of the counter-model generation algorithm for pseudo-atomic sequents.
- 1:
- INRIA – CNRS : UMR7503 – Université Henri Poincaré - Nancy I – Université Nancy II – Institut National Polytechnique de Lorraine (INPL)
- Domain : Computer Science/Logic in Computer Science
Computer Science/Artificial Intelligence
- hal-00008804, version 1
- http://hal.archives-ouvertes.fr/hal-00008804
- oai:hal.archives-ouvertes.fr:hal-00008804
- From:
- Submitted on: Friday, 16 September 2005 14:16:12
- Updated on: Tuesday, 29 March 2011 17:13:04
Export