Finding Finite Models in Multi-Sorted First-Order Logic

Giles Reger; Martin Suda; Andrei Voronkov

doi:10.1007/978-3-319-40970-2_20

Finding Finite Models in Multi-Sorted First-Order Logic

Giles Reger, Martin Suda, Andrei Voronkov

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

169 Downloads (Pure)

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 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.

Original language	English
Title of host publication	Theory and applications of satisfiability testing -- SAT 2016 : 19th International Conference, Bordeaux, France, July 5-8, 2016, Proceedings
Editors	Nadia Creuignou, Daniel Le Berre
Place of Publication	Cham
Publisher	Springer Nature
Pages	323-341
ISBN (Print)	9783319409696
DOIs	https://doi.org/10.1007/978-3-319-40970-2_20
Publication status	Published - 11 Jun 2016

Publication series

Name	Theory and Applications of Satisfiability Testing – SAT 2016
Publisher	Springer Nature
Volume	9710
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Access to Document

10.1007/978-3-319-40970-2_20

mainAccepted author manuscript, 297 KB

Cite this

Reger, G., Suda, M., & Voronkov, A. (2016). Finding Finite Models in Multi-Sorted First-Order Logic. In N. Creuignou, & D. Le Berre (Eds.), Theory and applications of satisfiability testing -- SAT 2016 : 19th International Conference, Bordeaux, France, July 5-8, 2016, Proceedings (pp. 323-341). (Theory and Applications of Satisfiability Testing – SAT 2016; Vol. 9710). Springer Nature. https://doi.org/10.1007/978-3-319-40970-2_20

Reger, Giles ; Suda, Martin ; Voronkov, Andrei. / Finding Finite Models in Multi-Sorted First-Order Logic. Theory and applications of satisfiability testing -- SAT 2016 : 19th International Conference, Bordeaux, France, July 5-8, 2016, Proceedings . editor / Nadia Creuignou ; Daniel Le Berre. Cham : Springer Nature, 2016. pp. 323-341 (Theory and Applications of Satisfiability Testing – SAT 2016).

@inproceedings{c82e7b14966b47ea98aa838e44088396,

title = "Finding Finite Models in Multi-Sorted First-Order Logic",

abstract = "This work extends the existing MACE-style finite model finding approachto multi-sorted first-order logic. This existing approach iteratively assumesincreasing domain sizes and encodes the related ground problem as a SATproblem. When moving to the multi-sorted setting each sort may have a differentdomain size, leading to an explosion in the search space. This paper focusses onmethods to tame that search space. The key approach adds additional informationto the SAT encoding to suggest which domains should be grown. Evaluation ofan implementation of techniques in the Vampire theorem prover shows that theydramatically reduce the search space and that this is an effective approach to findfinite models in multi-sorted first-order logic.",

author = "Giles Reger and Martin Suda and Andrei Voronkov",

year = "2016",

month = jun,

day = "11",

doi = "10.1007/978-3-319-40970-2_20",

language = "English",

isbn = "9783319409696",

series = "Theory and Applications of Satisfiability Testing – SAT 2016",

publisher = "Springer Nature",

pages = "323--341",

editor = "Nadia Creuignou and {Le Berre}, Daniel",

booktitle = "Theory and applications of satisfiability testing -- SAT 2016 : 19th International Conference, Bordeaux, France, July 5-8, 2016, Proceedings",

address = "United States",

}

Reger, G, Suda, M & Voronkov, A 2016, Finding Finite Models in Multi-Sorted First-Order Logic. in N Creuignou & D Le Berre (eds), Theory and applications of satisfiability testing -- SAT 2016 : 19th International Conference, Bordeaux, France, July 5-8, 2016, Proceedings . Theory and Applications of Satisfiability Testing – SAT 2016, vol. 9710, Springer Nature, Cham, pp. 323-341. https://doi.org/10.1007/978-3-319-40970-2_20

Finding Finite Models in Multi-Sorted First-Order Logic. / Reger, Giles; Suda, Martin; Voronkov, Andrei.
Theory and applications of satisfiability testing -- SAT 2016 : 19th International Conference, Bordeaux, France, July 5-8, 2016, Proceedings . ed. / Nadia Creuignou; Daniel Le Berre. Cham: Springer Nature, 2016. p. 323-341 (Theory and Applications of Satisfiability Testing – SAT 2016; Vol. 9710).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - Finding Finite Models in Multi-Sorted First-Order Logic

AU - Reger, Giles

AU - Suda, Martin

AU - Voronkov, Andrei

PY - 2016/6/11

Y1 - 2016/6/11

N2 - This work extends the existing MACE-style finite model finding approachto multi-sorted first-order logic. This existing approach iteratively assumesincreasing domain sizes and encodes the related ground problem as a SATproblem. When moving to the multi-sorted setting each sort may have a differentdomain size, leading to an explosion in the search space. This paper focusses onmethods to tame that search space. The key approach adds additional informationto the SAT encoding to suggest which domains should be grown. Evaluation ofan implementation of techniques in the Vampire theorem prover shows that theydramatically reduce the search space and that this is an effective approach to findfinite models in multi-sorted first-order logic.

AB - This work extends the existing MACE-style finite model finding approachto multi-sorted first-order logic. This existing approach iteratively assumesincreasing domain sizes and encodes the related ground problem as a SATproblem. When moving to the multi-sorted setting each sort may have a differentdomain size, leading to an explosion in the search space. This paper focusses onmethods to tame that search space. The key approach adds additional informationto the SAT encoding to suggest which domains should be grown. Evaluation ofan implementation of techniques in the Vampire theorem prover shows that theydramatically reduce the search space and that this is an effective approach to findfinite models in multi-sorted first-order logic.

U2 - 10.1007/978-3-319-40970-2_20

DO - 10.1007/978-3-319-40970-2_20

M3 - Conference contribution

SN - 9783319409696

T3 - Theory and Applications of Satisfiability Testing – SAT 2016

SP - 323

EP - 341

BT - Theory and applications of satisfiability testing -- SAT 2016 : 19th International Conference, Bordeaux, France, July 5-8, 2016, Proceedings

A2 - Creuignou, Nadia

A2 - Le Berre, Daniel

PB - Springer Nature

CY - Cham

ER -

Reger G, Suda M, Voronkov A. Finding Finite Models in Multi-Sorted First-Order Logic. In Creuignou N, Le Berre D, editors, Theory and applications of satisfiability testing -- SAT 2016 : 19th International Conference, Bordeaux, France, July 5-8, 2016, Proceedings . Cham: Springer Nature. 2016. p. 323-341. (Theory and Applications of Satisfiability Testing – SAT 2016). doi: 10.1007/978-3-319-40970-2_20

Finding Finite Models in Multi-Sorted First-Order Logic

Abstract

Publication series

Access to Document

Fingerprint

Cite this