Skip to Main content Skip to Navigation
Conference papers

Abstract Canonical Inference Systems

Nachum Dershowitz Claude Kirchner 1
1 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : We provide a general proof theoretical setting under which the so-called ``completion processes'' (as used for equational reasoning) can be modeled, understood, studied, proved and generalized. This framework---based on a well-founded ordering on proofs---allows us to derive saturation processes and redundancy criteria abstractly.
Mots-clés : abstract inference completion process proof ordering saturation redundancy ordre sur les preuves redondance inférence abstraite processus de complétion
Document type :
Conference papers
Complete list of metadata
https://hal.inria.fr/inria-00107627
Contributor : Publications Loria Connect in order to contact the contributor
Submitted on : Thursday, October 19, 2006 - 9:03:24 AM
Last modification on : Friday, February 26, 2021 - 3:28:06 PM
Long-term archiving on: : Wednesday, March 29, 2017 - 12:50:16 PM

File

Vignette du document
A02-R-501.pdf

Identifiers

  • HAL Id : inria-00107627, version 1

Collections

CNRS | INRIA | LORIA | UNIV-LORRAINE

Citation

Nachum Dershowitz, Claude Kirchner. Abstract Canonical Inference Systems. 16th International Workshop on Unification - UNIF'2002, Jul 2002, Copenhagen, Denmark, 20 p. ⟨inria-00107627⟩

Export

BibTeX TEI DC DCterms EndNote

Share

Metrics

Les métriques sont temporairement indisponibles

 

Contact                    Legal Notice                    Personal Data