iProver-Eq: An Instantiation-Based Theorem Prover with Equality

DOI10.1007/978-3-642-14203-1_17zbMath1291.68354OpenAlexW1520118813MaRDI QIDQ5747761

Christoph Sticksel, Konstantin Korovin

Publication date: 14 September 2010

Published in: Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-14203-1_17

Mathematics Subject Classification ID

Related Items

Semantically-guided goal-sensitive reasoning: model representation, History and Prospects for First-Order Automated Deduction, Exploring Theories with a Model-Finding Assistant, Semantically-guided goal-sensitive reasoning: inference system and completeness, Inst-Gen – A Modular Approach to Instantiation-Based Automated Reasoning, The Relative Power of Semantics and Unification, SCL(EQ): SCL for first-order logic with equality, Reducing higher-order theorem proving to a sequence of SAT problems

Uses Software

• cvc3
• z3
• iProver-Eq
• iProver

Cites Work

• iProver – An Instantiation-Based Theorem Prover for First-Order Logic (System Description)
• Computer Science Logic
• Theory and Applications of Satisfiability Testing