The CADE-27 Automated theorem proving System Competition – CASC-27

DOI10.3233/AIC-190627zbMath1464.68433OpenAlexW3010230113MaRDI QIDQ5145460

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-190627

zbMATH Keywords

competitionautomated theorem proving

Mathematics Subject Classification ID

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

Related Items (11)

The CADE-28 Automated Theorem Proving System Competition – CASC-28 ⋮ \( \alpha \)-paramodulation method for a lattice-valued logic \(L_nF(X)\) with equality ⋮ A multi-clause dynamic deduction algorithm based on standard contradiction separation rule ⋮ Unnamed Item ⋮ Superposition with lambdas ⋮ Making higher-order superposition work ⋮ Making higher-order superposition work ⋮ Preface: Special issue of selected extended papers of CADE 2019 ⋮ Guiding an automated theorem prover with neural rewriting ⋮ The 10th IJCAR automated theorem proving system competition – CASC-J10 ⋮ SAT-Inspired Eliminations for Superposition

Uses Software

• MiniSat
• TPTP
• HOL
• StarExec
• CVC4

Cites Work

• Mechanizing \(\omega\)-order type theory through unification
• Designing theory solvers with extensions
• Enhancing ENIGMA given clause guidance
• Efficient encodings of first-order Horn formulas in equational logic
• The CADE-16 ATP system competition
• Frontiers of combining systems. 12th international symposium, FroCoS 2019, London, UK, September 4--6, 2019. Proceedings
• Automated deduction -- CADE 27. 27th international conference on automated deduction, Natal, Brazil, August 27--30, 2019. Proceedings
• Extending SMT solvers to higher-order logic
• Restricted combinatory unification
• GRUNGE: a grand unified ATP challenge
• Old or heavy? Decaying gracefully with age/weight shapes
• Premise selection for mathematics by corpus analysis and kernel methods
• The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
• Performance of Clause Selection Heuristics for Saturation-Based Theorem Proving
• Overview and Evaluation of Premise Selection Techniques for Large Theory Mathematics
• Solving SAT and SAT Modulo Theories
• A Brief Overview of HOL4
• Using the TPTP Language for Writing Derivations and Finite Interpretations
• The 9th IJCAR Automated Theorem Proving System Competition – CASC-J9
• Sine Qua Non for Large Theory Reasoning

This page was built for publication: The CADE-27 Automated theorem proving System Competition – CASC-27