The CADE-28 Automated Theorem Proving System Competition – CASC-28

DOI10.3233/AIC-210235zbMath1487.68249OpenAlexW4220713172WikidataQ113701303 ScholiaQ113701303MaRDI QIDQ5069650

Martin Desharnais, Geoff Sutcliffe

Publication date: 19 April 2022

Published in: AI Communications (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.3233/aic-210235

zbMATH Keywords

competitionautomated theorem proving

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (2)

The 11th IJCAR automated theorem proving system competition – CASC-J11 ⋮ SAT-Inspired Higher-Order Eliminations

Uses Software

• MiniSat
• TPS
• VAMPIRE
• TPTP
• z3
• Sledgehammer
• StarExec
• iProver
• Easychair
• Waldmeister
• Twee

Cites Work

• Unnamed Item
• Unnamed Item
• TPS: A hybrid automatic-interactive system for developing proofs
• Critical pair criteria for completion
• Evaluating general purpose automated theorem proving systems
• The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0
• Efficient encodings of first-order Horn formulas in equational logic
• An abstraction-refinement framework for reasoning with large theories
• TPS: A theorem-proving system for classical type theory
• The CADE-16 ATP system competition
• Superposition for full higher-order logic
• Twee: an equational theorem prover
• Heterogeneous heuristic optimisation and scheduling for first-order theorem proving
• AC simplifications and closure redundancies in the superposition calculus
• Faster, higher, stronger: E 2.3
• Satallax: An Automatic Higher-Order Prover
• iProver – An Instantiation-Based Theorem Prover for First-Order Logic (System Description)
• The 7th IJCAR automated theorem proving system competition – CASC-J7
• Simple and Efficient Clause Subsumption with Feature Vector Indexing
• Inst-Gen – A Modular Approach to Instantiation-Based Automated Reasoning
• The 10th IJCAR automated theorem proving system competition – CASC-J10
• Implementing Superposition in iProver (System Description)
• The CADE-27 Automated theorem proving System Competition – CASC-27
• Theory and Applications of Satisfiability Testing
• Making higher-order superposition work
• Formalizing Bachmair and Ganzinger's ordered resolution prover

This page was built for publication: The CADE-28 Automated Theorem Proving System Competition – CASC-28