Decidable Fragments of Many-Sorted Logic

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

Mathematics Subject Classification ID

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

• 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