Blocking and Other Enhancements for Bottom-Up Model Generation Methods
Date
2019-03-01
Authors
Baumgartner, Peter
Schmidt, Renate A.
Journal Title
Journal ISSN
Volume Title
Publisher
Springer Netherlands
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, for example. This paper discusses several ways of enhancing the paradigm
of bottom-up model generation, with the two main contributions being a new range-restriction
transformation and generalized blocking techniques. The range-restriction transformation
refines existing transformations to range-restricted clauses by carefully limiting the creation
of domain terms. The blocking techniques are based on simple transformations of the input
set together with standard equality reasoning and redundancy elimination techniques, and
allow for finding small, finite models. All possible combinations of the introduced techniques and a classical range-restriction technique 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 that it is an indispensable technique for bottom-up model generation
methods, that yields good results in combination with both new and classical range-restricting
transformations. 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 show
bottom-up model generation methods are good for disproving theorems and generating models for satisfiable problems, but less efficient for unsatisfiable problems.
Description
Keywords
Automated reasoning, Model generation, Blocking, First-order logic, Bernays–Schönfinkel class
Citation
Collections
Source
Journal of Automated Reasoning
Type
Journal article
Book Title
Entity type
Access Statement
Open Access