Equational logic is one of the most important domains of research in computer science. Therefore, automated deduction in equational logic an important subject of research. However, the seemingly insurmountable search space caused by the symmetry and replacement properties of the equality predicate had been a serious obstacle which baffled researchers in automated deduction for several decades. It is not until very recently that methods capable of effectively reason with equations have been designed and successfully applied to an interesting range of challenging problems. These methods are based on the term rewriting approach to equational reasoning. The key idea in term rewriting based theorem proving is to regard a derivation as a process of proof reduction. Equations are oriented into rules according to a well-founded ordering, and equational replacement is performed only in one direction. By keeping every piece of data fully simplified at all time, the search space is drastically reduced.
High performance simplification-based automated deduction
BONACINA, Maria Paola
;
1992-01-01
Abstract
Equational logic is one of the most important domains of research in computer science. Therefore, automated deduction in equational logic an important subject of research. However, the seemingly insurmountable search space caused by the symmetry and replacement properties of the equality predicate had been a serious obstacle which baffled researchers in automated deduction for several decades. It is not until very recently that methods capable of effectively reason with equations have been designed and successfully applied to an interesting range of challenging problems. These methods are based on the term rewriting approach to equational reasoning. The key idea in term rewriting based theorem proving is to regard a derivation as a process of proof reduction. Equations are oriented into rules according to a well-founded ordering, and equational replacement is performed only in one direction. By keeping every piece of data fully simplified at all time, the search space is drastically reduced.File | Dimensione | Formato | |
---|---|---|---|
ACAMC1991simp.pdf
accesso aperto
Descrizione: Articolo
Tipologia:
Documento in Post-print
Licenza:
Creative commons
Dimensione
169.29 kB
Formato
Adobe PDF
|
169.29 kB | Adobe PDF | Visualizza/Apri |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.