On distinguishing sets of structures by first-order sentences of minimal quantifier rank. (English) Zbl 1434.03090
Accattoli, Beniamino (ed.) et al., Proceedings of the 13th workshop on logical and semantic frameworks with applications, LSFA 18, Fortaleza, Brazil, September 26–28, 2018. Amsterdam: Elsevier. Electron. Notes Theor. Comput. Sci. 344, 189-208 (2019).
Summary: We investigate the distinguishability of sets of relational structures concerning a class of structures in the following sense: for a fixed class of structures, given two sets of structures in this class, find a first-order formula of minimal quantifier rank that distinguishes one set from the other. We consider the following classes of structures: monadic structures, equivalence structures, and disjoint unions of linear orders. We use results of the Ehrenfeucht-Fraïssé game on these classes of structures in order to design an algorithm to find such a sentence. For these classes of structures, the problem of determining if the Duplicator has a winning strategy in an Ehrenfeucht-Fraïssé game is solved in polynomial time. We also introduce the distinguishability sentences which are sentences that distinguish between two given structures. We define the distinguishability sentences based on necessary and sufficient conditions for a winning strategy in an Ehrenfeucht-Fraïssé game. Our algorithm returns a Boolean combination of such sentences. We also show that any first-order sentence is equivalent to a Boolean combination of distinguishability sentences. Finally, we also show that our algorithm’s running time is polynomial in the size of the input.
For the entire collection see [Zbl 1420.68005].
For the entire collection see [Zbl 1420.68005].
References:
| [1] | Büchi, Richard J., Weak second-order arithmetic and finite automata, Zeitschrift für Mathematische Logik und Grundlagen der Mathematik, 6, 1-6, 66-92 (1960) · Zbl 0103.24705 |
| [2] | Cook, Stephen A.; Liu, Yongmei, A complete axiomatization for blocks world, Journal of Logic and Computation, 13, 4, 581-594 (2003) · Zbl 1046.68101 |
| [3] | De Raedt, Luc, Logical and Relational Learning (2008), Springer · Zbl 1203.68145 |
| [4] | Ebbinghaus, Heinz-Dieter; Flum, Jörg, Finite Model Theory (1995), Springer · Zbl 0841.03014 |
| [5] | Ebbinghaus, Heinz-Dieter; Flum, Jörg; Thomas, Wolfgang, Mathematical Logic (1994), Springer · Zbl 0852.03001 |
| [6] | Ehrenfeucht, Andrzej, An application of games to the completeness problem for formalized theories, Fundamenta Mathematicae, 49, 2, 129-141 (1961) · Zbl 0096.24303 |
| [7] | Ghallab, Malik; Nau, Dana; Traverso, Paolo, Automated Planning: Theory and Practice (2004), Elsevier · Zbl 1074.68613 |
| [8] | Grädel, Erich; Kolaitis, P. G.; Libkin, L.; Marx, M.; Spencer, J.; Vardi, Moshe Y.; Venema, Y.; Weinstein, Scott, Finite Model Theory and Its Applications (2005), Springer |
| [9] | Grohe, Martin; Löding, Christof; Ritzert, Martin, Learning MSO-definable hypotheses on strings, (International Conference on Algorithmic Learning Theory (2017), PMLR), 434-451 · Zbl 1403.68094 |
| [10] | Grohe, Martin; Ritzert, Martin, Learning first-order definable concepts over structures of small degree, (2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) (2017), IEEE), 1-12 · Zbl 1457.68133 |
| [11] | Gupta, Naresh; Nau, Dana S., On the complexity of blocks-world planning, Artificial Intelligence, 56, 2-3, 223-254 (1992) · Zbl 0785.68046 |
| [12] | Heule, Marijn; Verwer, Sicco, Exact DFA identification using SAT solvers, (International Colloquium on Grammatical Inference (2010), Springer), 66-79 · Zbl 1291.68192 |
| [13] | Jordan, Charles; Kaiser, Łukasz, Experiments with reduction finding, (International Conference on Theory and Applications of Satisfiability Testing (2013), Springer), 192-207 · Zbl 1390.68349 |
| [14] | Kaiser, Łukasz, Learning games from videos guided by descriptive complexity, (Proceedings of the Twenty-Sixth AAAI Conference on Artificial Intelligence (2012), AAAI Press), 963-969 |
| [15] | Khoussainov, Bakhadyr; Liu, Jiamou, On complexity of Ehrenfeucht-Fraïssé games, Annals of Pure and Applied Logic, 161, 3, 404-415 (2009) · Zbl 1221.03024 |
| [16] | Ladner, Richard E., Application of model theoretic games to discrete linear orders and finite automata, Information and Control, 33, 4, 281-303 (1977) · Zbl 0387.68037 |
| [17] | Libkin, Leonid, Elements Of Finite Model Theory (2004), Springer · Zbl 1060.03002 |
| [18] | De Maria, Elisabetta; Montanari, Angelo; Vitacolonna, Nicola, Games on strings with a limited order relation, (International Symposium on Logical Foundations of Computer Science (2009), Springer), 164-179 · Zbl 1211.03050 |
| [19] | Montanari, Angelo; Policriti, Alberto; Vitacolonna, Nicola, An algorithmic account of Ehrenfeucht games on labeled successor structures, (Logic for Programming, Artificial Intelligence, and Reasoning (2005), Springer), 139-153 · Zbl 1143.03353 |
| [20] | Muggleton, Stephen, Inductive logic programming, New Generation Computing, 8, 4, 295-318 (1991) · Zbl 0712.68022 |
| [21] | Muggleton, Stephen; De Raedt, Luc, Inductive logic programming: Theory and methods, The Journal of Logic Programming, 19, 629-679 (1994) · Zbl 0816.68043 |
| [22] | Pezzoli, Elena, Computational complexity of Ehrenfeucht-Fraïssé games on finite structures, (Computer Science Logic (1999), Springer), 159-170 · Zbl 0934.03048 |
| [23] | Alves Rocha, Thiago; Teresa Martins, Ana; Martins Ferreira, Francicleber, On finding a first-order sentence consistent with a sample of strings, (International Symposium on Games, Automata, Logics, and Formal Verification (2018), Open Publishing Association), 220-234 · Zbl 1528.68198 |
| [24] | Thomas, Wolfgang, Classifying regular events in symbolic logic, Journal of Computer and System Sciences, 25, 3, 360-376 (1982) · Zbl 0503.68055 |
| [25] | Zakirzyanov, Ilya; Shalyto, Anatoly; Ulyantsev, Vladimir, Finding all minimum-size DFA consistent with given examples: SAT-based approach, (International Conference on Software Engineering and Formal Methods (2017), Springer), 117-131 · Zbl 1461.68110 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
