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

DOI10.3233/AIC-210235MaRDI QIDQ5069650zbMATH OpenOpenAlexWikidataFDO

Authors 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)

Cites work

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

Cited in

(3)

• SAT-Inspired Higher-Order Eliminations
• scientific article; zbMATH DE number 5305114 (Why is no real title available?)
• The 11th IJCAR automated theorem proving system competition – CASC-J11

Describes a project that uses

Uses Software

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

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5069650)