T. Kutsia. Theorem proving with sequence variables and flexible arity symbols. volume 2514, pages 278-291, 2002.
|Buch||Logic for Programming, Artificial Intelligence, and Reasoning.|
|Serie||Lecture Notes in Artificial Intelligence|
||An ordering for terms with sequence variables and flexible arity symbols is presented. The ordering coincides with the lexicographic extension of multiset path ordering on terms without sequence variables. It is shown that the classical strict superposition calculus with ordering and equality constraints can be used as a refutationally complete proving method for well-constrained sets of clauses with sequence variables and flexible arity symbols.