Decidable fragments of many-sorted logic

Decidable fragments of many-sorted logic,10.1016/j.jsc.2009.03.003,Journal of Symbolic Computation,Aharon Abadi,Alexander Rabinovich,Mooly Sagiv

Decidable fragments of many-sorted logic   (Citations: 3)
BibTex | RIS | RefWorks Download
Many natural specifications use types. We investigate the decidability of fragments of many-sorted first-order logic. We identified some decidable fragments and illustrated their usefulness by formalizing specifications considered in the literature. Often the intended interpretations of specifications are finite. We prove that the formulas in these fragments are valid iff they are valid over the finite structures. We extend these results to logics that allow a restricted form of transitive closure.We tried to extend the classical classification of the quantifier prefixes into decidable/undecidable classes to the many-sorted logic. However, our results indicate that a naive extension fails and more subtle classification is needed.
Journal: Journal of Symbolic Computation - JSC , vol. 45, no. 2, pp. 153-172, 2010
Cumulative Annual
View Publication
The following links allow you to view full publications. These links are maintained by other sources not affiliated with Microsoft Academic Search.
    • ...The results in this section concern decidable subclasses of first-order logic with sorts, which are investigated in [1]...
    • ...This instantiation scheme can be applied also to the class St2 defined in [1] as an extension of the class St0 with atoms of the form t ∈ Im[f ], where f is a function symbol of profile s1 × ... ×sn → s, meaning that t is in the image of the function f . From a semantic point of view, the atom t ∈ Im[f ] is a shorthand for ∃x1 ,...,x n.t � f (x1 ,...,x n). To ensure decidability, for every atom of the form t ∈ Im[f ] and for ...
    • ...In [1] it is shown that every satisfiable set in St2 admits a finite model, hence, St2 is decidable...
    • ...Examples of specifications in the classes St0 and St2 are presented in [1]...
    • ...Provided the integer variables essentially occur in inequality constraints, this scheme is complete for the combination of linear arithmetic with several theories of interest to the SMT community, but also for the combination of linear arithmetic with other decidable theories such as the class St2 from [1]...

    Mnacho Echenimet al. Instantiation of SMT Problems Modulo Integers

Sort by: