Theorem proving with sequence variables and flexible arity symbols

T. Kutsia. Theorem proving with sequence variables and flexible arity symbols. volume 2514, pages 278-291, 2002.

Autoren
  • Teimuraz Kutsia
Editoren
  • M. Baaz
  • A. Voronkov
BuchLogic for Programming, Artificial Intelligence, and Reasoning.
TypIn Sammelband
VerlagSpringer
SerieLecture Notes in Artificial Intelligence
Band2514
ISBN3-540-00010-0
Jahr2002
Seiten278-291
Abstract 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.