A First-order Simplification Rule with Constraints

Martin Giese

Several variants of a first-order simplification rule for non-normal
form tableaux using syntactic constraints are presented.  These can be
used as a framework for porting refinements of clausal first-order
proof procedures to non-normal form tableaux.  Some experimental
results obtained with a prototypical implementation are given.