@TECHREPORT{BaumgartnerSchmidt16TR,
AUTHOR = {Baumgartner, P. and Schmidt, R. A.},
YEAR = {2016},
TITLE = {Blocking and Other Enhancements for Bottom-Up Model Generation Methods},
TYPE = {arXiv e-Print},
NUMBER = {1611.09014 [cs.AI]},
URL = {http://arxiv.org/abs/1611.09014},
ABSTRACT = {Model generation is a problem complementary to theorem proving 
and is important for fault analysis and debugging of formal specifications 
of security protocols, programs and terminological definitions. This paper 
discusses several ways of enhancing the paradigm of bottom-up model 
generation. The two main contributions are new, generalized blocking 
techniques and a new range-restriction transformation. The blocking 
techniques are based on simple transformations of the input set together
with standard equality reasoning and redundancy elimination techniques. 
These provide general methods for finding small, finite models. The 
range-restriction transformation refines existing transformations to 
range-restricted clauses by carefully limiting the creation of domain terms. 
All possible combinations of the introduced techniques and classical 
range-restriction were tested on the clausal problems of the TPTP Version 6.0.0 
with an implementation based on the SPASS theorem prover using a 
hyperresolution-like refinement. Unrestricted domain blocking gave best 
results for satisfiable problems showing it is a powerful technique 
indispensable for bottom-up model generation methods. Both in combination 
with the new range-restricting transformation, and the classical 
range-restricting transformation, good results have been obtained. 
Limiting the creation of terms during the inference process by using the 
new range restricting transformation has paid off, especially when using 
it together with a shifting transformation. The experimental results also 
show that classical range restriction with unrestricted blocking provides 
a useful complementary method. Overall, the results showed bottom-up model 
generation methods were good for disproving theorems and generating 
models for satisfiable problems, but less efficient than SPASS in auto 
mode for unsatisfiable problems.
}
}