Para acceder a los documentos con el texto completo, por favor, siga el siguiente enlace: http://hdl.handle.net/2117/93071

Título:	Maximal strategies for paramodulation with non-monotonic orderings
Autor/a:	Bofill Arasa, Miquel; Godoy Balil, Guillem
Otros autores:	Universitat Politècnica de Catalunya. Departament de Ciències de la Computació; Universitat Politècnica de Catalunya. LOGPROG - Lògica i Programació
Abstract:	A west ordering is a well-founded (strict partial) ordering on terms that satisfies the subterm property. In [Bofill, Godoy, Nieuwenhuis, Rubio, (BGNR-LICS99)] the completeness of an ordered paramodulation inference system w.r.t. west orderings was proved, thus dropping for the first time the monotonicity requirements on the ordering. However, the inference system still required the eager selection of negative equations. Here we improve upon [BGNR-LICS99] in two directions. On the one hand, we show that the results are compatible with constraint inheritance and the so-called basic strategy [(Bachmair, Ganzinger, Lynch, Snyder (1995IC)), (Nieuwenhuis, Rubio (1995JSC))], thus further restricting the search space. On the other hand, we introduce an inference system where also the positive equations of non-unit clauses can be selected, provided that they are maximal.
Materia(s):	-Àrees temàtiques de la UPC::Informàtica
Derechos:
Tipo de documento:	Artículo - Versión publicada Informe
Compartir:

Mostrar el registro completo del ítem