Decidable Fragments of Many-Sorted Logic

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

Mathematics Subject Classification ID

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

• VAMPIRE

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