inria-00099056, version 1
Sequent Calculus Viewed Modulo
12th European Summer School in Logic, Language & Information - ESSLLI'2000 Student Session (2000) 11 p
Abstract: The first-order sequent calculus is generally considered as containing no computation but only pure deduction. But this is not completely true if we look at it carefully, using a deduction modulo framework. The origins of the computational part are first implicit behaviours of the calculus, then well known consequences that we do not want to prove any more. We end up with a calculus fully in the spirit of deduction modulo.
- a – 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 : deduction modulo – first-order logic – sequent calculus || déduction modulo – logique du premier ordre – calcul des séquents
- Internal note : A00-R-256 || deplagne00a
- Comment : Colloque avec actes et comité de lecture. internationale.
- inria-00099056, version 1
- http://hal.inria.fr/inria-00099056
- oai:hal.inria.fr:inria-00099056
- From:
- Submitted on: Tuesday, 26 September 2006 08:48:51
- Updated on: Thursday, 28 September 2006 15:22:45
Export