An abstract framework of canonical inference is used to explore how different proof orderings induce different variants of saturation and completeness. Notions like completion, paramodulation, saturation, redundancy elimination, and rewrite-system reduction are connected to proof orderings. Fairness of deductive mechanisms is defined in terms of proof orderings, distinguishing between (ordinary) ``fairness,'' which yields completeness, and ``uniform fairness,'' which yields saturation.
Abstract canonical inference
BONACINA, Maria Paola
;
2007-01-01
Abstract
An abstract framework of canonical inference is used to explore how different proof orderings induce different variants of saturation and completeness. Notions like completion, paramodulation, saturation, redundancy elimination, and rewrite-system reduction are connected to proof orderings. Fairness of deductive mechanisms is defined in terms of proof orderings, distinguishing between (ordinary) ``fairness,'' which yields completeness, and ``uniform fairness,'' which yields saturation.
File in questo prodotto:
| File | Dimensione | Formato | |
|---|---|---|---|
|
TOCL2007canonicity.pdf
accesso aperto
Descrizione: Articolo
Tipologia:
Documento in Post-print
Licenza:
Creative commons
Dimensione
260.86 kB
Formato
Adobe PDF
|
260.86 kB | Adobe PDF | Visualizza/Apri |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
