Decidable Fragments of Many-Sorted Logic
From MaRDI portal
Publication:3498453
DOI10.1007/978-3-540-75560-9_4zbMath1137.03302OpenAlexW2166403227MaRDI QIDQ3498453
Mooly Sagiv, Aharon Abadi, Alexander Rabinovich
Publication date: 15 May 2008
Published in: Logic for Programming, Artificial Intelligence, and Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-540-75560-9_4
Specification and verification (program logics, model checking, etc.) (68Q60) Classical first-order logic (03B10) Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35)
Related Items
Decidable Fragments of Many-Sorted Logic ⋮ Lattice logic as a fragment of (2-sorted) residuated modal logic ⋮ Decidable \({\exists}^*{\forall}^*\) first-order fragments of linear rational arithmetic with uninterpreted predicates ⋮ Decidable fragments of many-sorted logic
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Decidable verification for reducible timed automata specified in a first order logic with time
- Decidable Fragments of Many-Sorted Logic
- The unsolvability of the Gödel class with identity
- On languages with two variables
- SPASS & FLOTTER version 0.42
- Automated Deduction – CADE-20
- Bounded model checking using satisfiability solving
- A first order logic for specification of timed algorithms: Basic properties and a decidable class