Abstract Canonical Inference Systems

Nachum Dershowitz , Claude Kirchner (1)

1 PROTHEO - Constraints, automatic deduction and software properties proofs

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: completion process; proof ordering; saturation; redundancy; ordre sur les preuves; redondance; inférence abstraite; abstract inference; processus de complétion

Domaines: Autre [cs.OH]

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