inria-00100204, version 1
Proving Theorems by Folding/Unfolding
2nd International Conference : Sciences of Electronic, Technologies of Information and Telecommunications - SETIT 2004 (2004) 6 p
Abstract: Proofs techniques can be seen as simplification methods, i.e. formulas are transformed into trivial ones, true. Unfortunately, we are sometimes faced with an unprovable formula because no induction hypothesis can be applied. In this paper, we propose a method that can allows us to apply induction hypothesis.
- a – FAC. DES SCIENCES DE TUNIS, DSI
- b – UNIVERSITE HENRI POINCARE
- 1:
- INRIA – CNRS : UMR7503 – Université Henri Poincaré - Nancy I – Université Nancy II – Institut National Polytechnique de Lorraine (INPL)
- Domain : Computer Science/Other
- Keywords : automated theorem proving – folding – unfolding – implicative formulas – mathematical induction || démonstration automatique – pliage – dépliage – formule implicative – induction mathématique
- Internal note : A04-R-566 || demba04b
- Comment : Colloque avec actes et comité de lecture. internationale.
- inria-00100204, version 1
- http://hal.inria.fr/inria-00100204
- oai:hal.inria.fr:inria-00100204
- From:
- Submitted on: Tuesday, 26 September 2006 10:15:29
- Updated on: Wednesday, 10 January 2007 16:50:54
Export