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.
Keywords: 
Issue
Pages: 
1-11
File: 
  
  
 anureev_6.pdf
 (274.45 KB)