Blocking and Other Enhancements for Bottom-Up Model Generation Methods
From MaRDI portal
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.
Recommendations
- Blocking and other enhancements for bottom-up model generation methods
- Generic constraint-based block modeling using constraint programming
- Model generation with Boolean constraints
- scientific article; zbMATH DE number 1088032
- scientific article; zbMATH DE number 1140609
- Efficient model generation through compilation
Cited in
(14)- Computing finite models by reduction to function-free clause logic
- A new methodology for developing deduction methods
- Blocking and other enhancements for bottom-up model generation methods
- A bi-intuitionistic modal logic: foundations and automation
- Simulation and synthesis of deduction calculi
- Exploring theories with a model-finding assistant
- Modal tableau systems with blocking and congruence closure
- On deciding satisfiability by theorem proving with speculative inferences
- Superposition for bounded domains
- Inst-Gen -- a modular approach to instantiation-based automated reasoning
- First-order resolution methods for modal logics
- Using tableau to decide description logics with full role negation and identity
- Optimized description logic reasoning via core blocking
- A resolution-based decision procedure for \({\mathcal{SHOIQ}}\).
This page was built for publication: Blocking and Other Enhancements for Bottom-Up Model Generation Methods
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3613405)
