Decidable fragments of many-sorted logic

DOI10.1016/j.jsc.2009.03.003zbMath1183.03007OpenAlexW1971727793MaRDI QIDQ1041587

Aharon Abadi, Mooly Sagiv, Alexander Rabinovich

Publication date: 3 December 2009

Published in: Journal of Symbolic Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.jsc.2009.03.003

zbMATH Keywords

verificationtransitive closuremany-sorted logicclassical decision problemdecidable logic

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Decidability of theories and sets of sentences (03B25)

Related Items (6)

A decidable and expressive fragment of Many-Sorted first-order linear temporal logic ⋮ Semantically-guided goal-sensitive reasoning: decision procedures and the Koala prover ⋮ Modular instantiation schemes ⋮ An instantiation scheme for satisfiability modulo theories ⋮ Decidable \({\exists}^*{\forall}^*\) first-order fragments of linear rational arithmetic with uninterpreted predicates ⋮ SGGS decision procedures

Uses Software

• Z

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Model theory
• Decidable verification for reducible timed automata specified in a first order logic with time
• Back to the future
• Decidable Fragments of Many-Sorted Logic
• The unsolvability of the Gödel class with identity
• On languages with two variables
• Computer Science Logic
• A first order logic for specification of timed algorithms: Basic properties and a decidable class

This page was built for publication: Decidable fragments of many-sorted logic