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

DOI10.3233/AIC-210235zbMATH Open1487.68249OpenAlexW4220713172WikidataQ113701303 ScholiaQ113701303MaRDI QIDQ5069650FDOQ5069650

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

• Theory and Applications of Satisfiability Testing
• Satallax: An Automatic Higher-Order Prover
• TPS: A hybrid automatic-interactive system for developing proofs
• Faster, higher, stronger: E 2.3
• Formalizing Bachmair and Ganzinger's ordered resolution prover
• Evaluating general purpose automated theorem proving systems
• TPS: A theorem-proving system for classical type theory
• iProver – An Instantiation-Based Theorem Prover for First-Order Logic (System Description)
• Inst-Gen -- a modular approach to instantiation-based automated reasoning
• Critical pair criteria for completion
• Ordered rewriting and confluence
• 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
• The CADE-16 ATP system competition
• Simple and Efficient Clause Subsumption with Feature Vector Indexing
• An abstraction-refinement framework for reasoning with large theories
• Superposition for full higher-order logic
• Twee: an equational theorem prover
• Title not available (Why is that?)
• The CADE-27 automated theorem proving system competition -- CASC-27
• Making higher-order superposition work
• Title not available (Why is that?)
• Heterogeneous heuristic optimisation and scheduling for first-order theorem proving
• AC simplifications and closure redundancies in the superposition calculus
• The 10th IJCAR automated theorem proving system competition -- CASC-J10
• Implementing Superposition in iProver (System Description)
• The 7th IJCAR automated theorem proving system competition -- CASC-J7

Cited In (3)

• SAT-Inspired Higher-Order Eliminations
• Title not available (Why is that?)
• The 11th IJCAR automated theorem proving system competition – CASC-J11

Uses Software

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

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)