Abstract:

A new notion of a multi-branch narrowing that allows case analysis to be built in is introduced. A narrowing strategy that preserves formula satisfiability is suggested. A formalism called formula rewriting systems specifying the strategy is defined. The termination of formula rewriting systems is considered.

DOI:
Issue
Pages:
1-11
File:
anureev_6.pdf (274.45 KB)