Non-cyclic Sorts for First-Order Satisfiability

DOI10.1007/978-3-642-40885-4_15zbMath1398.68484OpenAlexW2127882277MaRDI QIDQ2849491

Konstantin Korovin

Publication date: 20 September 2013

Published in: Frontiers of Combining Systems (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-40885-4_15

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Related Items

Semantically-guided goal-sensitive reasoning: decision procedures and the Koala prover ⋮ NRCL - A Model Building Approach to the Bernays-Schönfinkel Fragment ⋮ Decidable \({\exists}^*{\forall}^*\) first-order fragments of linear rational arithmetic with uninterpreted predicates ⋮ Model Finding for Recursive Functions in SMT ⋮ SCL clause learning from simple models ⋮ SGGS decision procedures

Uses Software

• TPTP
• iProver