Decidable Fragments of Many-Sorted Logic
From MaRDI portal
Publication:3498453
DOI10.1007/978-3-540-75560-9_4zbMath1137.03302MaRDI 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
68Q60: Specification and verification (program logics, model checking, etc.)
03B10: Classical first-order logic
03B25: Decidability of theories and sets of sentences
03B35: Mechanization of proofs and logical operations
Related Items
Lattice logic as a fragment of (2-sorted) residuated modal logic, Decidable fragments of many-sorted 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