Constructing infinite models represented by tree automata. (English) Zbl 1183.68562
Summary: We propose a method to use finite model builders in order to construct infinite models of first-order formulae. The constructed models are Herbrand interpretations, in which the interpretation of the predicate symbols is specified by tree tuple automata (Comon et al.). Our approach is based on formula transformation: a formula \(\varphi \) is transformed into a formula \(\Delta (\varphi )\) s.t. \(\varphi \) has a model representable by a term tuple automaton iff \(\Delta (\varphi )\) has a finite model. This paper is an extended version of the author’s paper in Lect. Notes Comput. Sci. 5144, 155–169 (2008; Zbl 1166.68352)].
MSC:
| 68T15 | Theorem proving (deduction, resolution, etc.) (MSC2010) |
| 03B35 | Mechanization of proofs and logical operations |
| 68Q45 | Formal languages and automata |
Keywords:
finite model buildersCitations:
Zbl 1166.68352References:
| [1] | Audemard, G., Benhamou, B., Henocque, L.: Predicting and detecting symmetries in fol finite model search. J. Autom. Reason. 36(3), 177–212 (2006) · Zbl 1107.68092 · doi:10.1007/s10817-006-9040-3 |
| [2] | Baumgartner, P.: FDPLL–a first-order Davis-Putnam-Logeman-Loveland procedure. In: McAllester, D. (ed.) CADE-17–The 17th International Conference on Automated Deduction. LNAI, vol. 1831, pp. 200–219. Springer, New York (2000) · Zbl 0963.68182 |
| [3] | Caferra, R., Leitsch, A., Peltier, N.: Automated Model Building. Applied Logic Series, vol. 31. Kluwer, Dordrecht (2004) · Zbl 1085.03009 |
| [4] | Caferra, R., Zabel, N.: A method for simultaneous search for refutations and models by equational constraint solving. J. Symb. Comput. 13, 613–641 (1992) · Zbl 0770.68104 · doi:10.1016/S0747-7171(10)80014-8 |
| [5] | Claessen, K., Sorensson, N.: New techniques that improve MACE-style finite model finding. In: Proceedings of the CADE-19 Workshop: Model Computation–Principles, Algorithms, Applications, Miami (2003) |
| [6] | Comon, H., Dauchet, M., Gilleron, R., Jacquemard, F., Lugiez, D., Tison, S., Tommasi, M.: Tree automata techniques and applications. http://www.grappa.univ-lille3.fr/tata (1997) |
| [7] | Fermueller, C., Pichler, R.: Model representation via contexts and implicit generalizations. In: CADE, pp. 409–423 (2005) · Zbl 1135.03327 |
| [8] | Fitting, M.: First-Order Logic and Automated Theorem Proving. Texts and Monographs in Computer Science. Springer, New York (1990) · Zbl 0692.68002 |
| [9] | Gottlob, G., Pichler, R.: Working with ARMs: Complexity results on atomic representations of Herbrand models. Inf. Comput. 165, 183–207 (2001) · Zbl 1007.03009 · doi:10.1006/inco.2000.2915 |
| [10] | McCune, B.: MACE 2.0 reference manual and guide. Technical report, Argonne National Laboratory (2001) |
| [11] | Peltier, N.: A new method for automated finite model building exploiting failures and symmetries. J. Log. Comput. 8(4), 511–543 (1998) · Zbl 0904.68155 · doi:10.1093/logcom/8.4.511 |
| [12] | Peltier, N.: Automated model building: From finite to infinite models. In: 9th International Conference on Artificial Intelligence and Symbolic Computation. LNCS, vol. 5144, pp. 155–169. Springer, New York (2008) · Zbl 1166.68352 |
| [13] | Plaisted, D., Greenbaum, S.: A structure-preserving clause form translation. J. Symbol. Comput. 2, 293–304 (1986) · Zbl 0636.68119 · doi:10.1016/S0747-7171(86)80028-1 |
| [14] | Slaney, J.: Finder: finite domain enumerator. In: Proc. of CADE-12. LNAI, vol. 814, pp. 798–801. Springer, New York (1994) |
| [15] | Zhang, J., Zhang, H.: System description: generating models by SEM. In: McRobbie, M.A., Slaney, J.K. (eds.) 13th International Conference on Automated Deduction. Lecture Notes in Computer Science, vol. 1104, pp. 308–312. Springer, New York (1996) |
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.
