The CADE-26 automated theorem proving system competition – CASC-26

DOI10.3233/AIC-170744zbMath1462.68219OpenAlexW2917421790MaRDI QIDQ5145427

Geoff Sutcliffe

Publication date: 20 January 2021

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

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

zbMATH Keywords

competitionautomated theorem proving

Mathematics Subject Classification ID

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

Related Items (2)

The 9th IJCAR Automated Theorem Proving System Competition – CASC-J9 ⋮ The 10th IJCAR automated theorem proving system competition – CASC-J10

Uses Software

• MiniSat
• TPTP
• Satallax
• Sledgehammer
• CakeML
• StarExec
• Easychair
• Leo-III
• kepler98

Cites Work

• Analytic tableaux for higher-order logic with choice
• A revision of the proof of the Kepler conjecture
• Theorem proving modulo
• The CADE-16 ATP system competition
• Reducing higher-order theorem proving to a sequence of SAT problems
• Finding proofs in Tarskian geometry
• A transfinite Knuth-Bendix order for lambda-free higher-order terms
• The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
• Agent-Based HOL Reasoning
• Satallax: An Automatic Higher-Order Prover
• The TPTP World – Infrastructure for Automated Reasoning
• Analytic Tableaux for Simple Type Theory and its First-Order Fragment
• A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification
• The 8th IJCAR automated theorem proving system competition – CASC-J8
• Simple and Efficient Clause Subsumption with Feature Vector Indexing
• Sine Qua Non for Large Theory Reasoning
• CakeML
• Towards Knowledge Management for HOL Light

This page was built for publication: The CADE-26 automated theorem proving system competition – CASC-26