Decidable fragments of many-sorted logic
From MaRDI portal
Publication:1041587
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
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
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