Carregant...
Carregant...

Vés al contingut (premeu Retorn)

Paramodulation with non-monotonic orderings and simplification

Autor
Bofill, M.; Rubio, A.
Tipus d'activitat
Article en revista
Revista
Journal of automated reasoning
Data de publicació
2013-01
Volum
50
Número
1
Pàgina inicial
51
Pàgina final
98
DOI
https://doi.org/10.1007/s10817-011-9244-z Obrir en finestra nova
Resum
Ordered paramodulation and Knuth-Bendix completion are known to remain complete when using non-monotonic orderings. However, these results do not imply the compatibility of the calculus with essential redundancy elimination techniques such as demodulation, i.e., simplification by rewriting, which constitute the primary mode of computation in most successful automated theorem provers. In this paper we present a complete ordered paramodulation calculus for non-monotonic orderings which is compatib...
Paraules clau
Automated theorem proving, Equational reasoning, Knuth-Bendix completion, Ordered paramodulation
Grup de recerca
LOGPROG - Lògica i Programació

Participants