Tree Automata and Automated Model Building

Article type: Research Article

Authors: Peltier, Nicolas

Affiliations: Leibmz-Imag, 46, Avenue Félix Viallet, 38031 Grenoble Cedex, France. Nicolas.Peltier@imag.fr

Abstract: The use of regular tree grammars to represent and build models of formulae of first-order logic without equality is investigated. The combination of regular tree grammars with equational constraints provides a powerful and general way of representing Herbrand models. We show that the evaluation problem (i.e. the problem of finding the truth value of a formula in a given model) is decidable when models are represented in the way we propose. We also define a method to build such representations of models for first-order formulae. These results are a powerful extension of our former method for simultaneous search for refutations and models.

Keywords: Automated Deduction, Model Building, Tree Automata, Regular Tree Grammars

DOI: 10.3233/FI-1997-30105

Journal: Fundamenta Informaticae, vol. 30, no. 1, pp. 59-81, 1997