To access the full text documents, please follow this link: http://hdl.handle.net/2117/93071

Title:	Maximal strategies for paramodulation with non-monotonic orderings
Author:	Bofill Arasa, Miquel; Godoy Balil, Guillem
Other authors:	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.
Subject(s):	-Àrees temàtiques de la UPC::Informàtica
Rights:
Document type:	Article - Published version Report
Share:

Show full item record