Notice
This item was automatically migrated from a legacy system. It's data has not been checked and might not meet the quality criteria of the present system.
Reger, G., Suda, M., & Voronkov, A. (2016). Finding Finite Models in Multi-sorted First-Order Logic. In Theory and Applications of Satisfiability Testing – SAT 2016 (pp. 323–341). Springer. https://doi.org/10.1007/978-3-319-40970-2_20
E192-04 - Forschungsbereich Formal Methods in Systems Engineering
-
Published in:
Theory and Applications of Satisfiability Testing – SAT 2016
-
Date (published):
2016
-
Event name:
19th International Conference on Theory and Applications of Satisfiability Testing, SAT 2016
-
Event date:
5-Jul-2016 - 8-Jul-2016
-
Event place:
Bordeaux, France, EU
-
Number of Pages:
19
-
Publisher:
Springer, LNCS 9710
-
Peer reviewed:
Yes
-
Keywords:
finite model finding; multi-sorted first-order logic; vampire
-
Abstract:
This work extends the existing MACE-style finite model finding approach to multi-sorted first order logic. This existing approach iteratively assumes increasing domain sizes and encodes the related ground problem as a SAT problem. When moving to the multi-sorted setting each sort may have a different domain size, leading to an explosion in the search space. This paper focusses on methods to tame t...
This work extends the existing MACE-style finite model finding approach to multi-sorted first order logic. This existing approach iteratively assumes increasing domain sizes and encodes the related ground problem as a SAT problem. When moving to the multi-sorted setting each sort may have a different domain size, leading to an explosion in the search space. This paper focusses on methods to tame that search space. The key approach adds additional information to the SAT encoding to suggest which domains should be grown. Evaluation of an implementation of techniques in the Vampire theorem prover shows that they dramatically reduce the search space and that this is an effective approach to find finite models in multi-sorted first order logic.
en
Research Areas:
Logic and Computation: 70% Computer Science Foundations: 30%
