First-Order Logic Theorem Proving and Model Building via Approximation and Instantiation

DOI10.1007/978-3-319-24246-0_6zbMath1471.03020arXiv1503.02971OpenAlexW1936712172MaRDI QIDQ2964455

Christoph Weidenbach, Andreas Teucke

Publication date: 27 February 2017

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

Full work available at URL: https://arxiv.org/abs/1503.02971

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35)

Related Items (3)

Automated Reasoning Building Blocks ⋮ SPASS-AR: a first-order theorem prover based on approximation-refinement into the monadic shallow linear fragment ⋮ SCL clause learning from simple models

Uses Software

• TPTP

Cites Work

• Unnamed Item
• Unnamed Item
• Explicit representation of terms defined by counter examples
• Theorem proving with abstraction
• A theory of abstraction
• Term-rewriting systems with rule priorities
• The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
• Solving SAT and SAT Modulo Theories
• Inst-Gen – A Modular Approach to Instantiation-Based Automated Reasoning

This page was built for publication: First-Order Logic Theorem Proving and Model Building via Approximation and Instantiation