Loading…

Abstract canonical presentations

Solving goals—like proving properties, deciding word problems or resolving constraints—is much easier with some presentations of the underlying theory than with others. Typically, what have been called “completion processes”, in particular in the study of equational logic, involve finding appropriat...

Full description

Saved in:
Bibliographic Details
Published in:Theoretical computer science 2006-07, Vol.357 (1), p.53-69
Main Authors: Dershowitz, Nachum, Kirchner, Claude
Format: Article
Language:English
Subjects:
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:Solving goals—like proving properties, deciding word problems or resolving constraints—is much easier with some presentations of the underlying theory than with others. Typically, what have been called “completion processes”, in particular in the study of equational logic, involve finding appropriate presentations of a given theory to more easily solve a given class of problems. We provide a general proof-theoretic setting that relies directly on the fundamental concept of “good”, that is, normal-form, proofs, itself defined using well-founded orderings on proof objects. This foundational framework allows for abstract definitions of canonical presentations and very general characterizations of saturation and redundancy criteria.
ISSN:0304-3975
1879-2294
DOI:10.1016/j.tcs.2006.03.012