Theorem proving with sequence variables and flexible arity symbols

Autoren Teimuraz Kutsia
Editoren M. Baaz
A. Voronkov
Titel Theorem proving with sequence variables and flexible arity symbols
Buchtitel Logic for Programming, Artificial Intelligence, and Reasoning.
Typ in Sammelband
Verlag Springer
Serie Lecture Notes in Artificial Intelligence
Band 2514
ISBN 3-540-00010-0
Jahr 2002
Seiten 278-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.