Theorem proving with sequence variables and flexible arity symbols

Autoren Teimuraz Kutsia
Editoren M. Baaz
A. Voronkov
TitelTheorem proving with sequence variables and flexible arity symbols
BuchtitelLogic for Programming, Artificial Intelligence, and Reasoning.
Typin Sammelband
VerlagSpringer
SerieLecture Notes in Artificial Intelligence
Band2514
ISBN3-540-00010-0
Jahr2002
Seiten278-291
SCCH ID#266
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.