The 9th IJCAR Automated Theorem Proving System Competition – CASC-J9

DOI10.3233/AIC-180773zbMath1462.68220OpenAlexW4249545655MaRDI QIDQ5145447

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

zbMATH Keywords

competitionautomated theorem proving

Mathematics Subject Classification ID

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

Related Items (7)

A multi-clause dynamic deduction algorithm based on standard contradiction separation rule ⋮ On structures of regular standard contradictions in propositional logic ⋮ The CADE-27 Automated theorem proving System Competition – CASC-27 ⋮ GRUNGE: a grand unified ATP challenge ⋮ Names are not just sound and smoke: word embeddings for axiom selection ⋮ Old or heavy? Decaying gracefully with age/weight shapes ⋮ GKC: a reasoning system for large knowledge bases

Uses Software

• TPTP
• CakeML
• StarExec
• nanoCoP

Cites Work

• Critical pair criteria for completion
• Evaluating general purpose automated theorem proving systems
• Non-clausal connection calculi for non-classical logics
• Efficient encodings of first-order Horn formulas in equational logic
• The CADE-16 ATP system competition
• Unification with abstraction and theory instantiation in saturation-based reasoning
• The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
• nanoCoP: A Non-clausal Connection Prover
• Selecting the Selection
• A Non-clausal Connection Calculus
• Blocked Clauses in First-Order Logic
• Simple and Efficient Clause Subsumption with Feature Vector Indexing
• The CADE-26 automated theorem proving system competition – CASC-26
• CakeML

This page was built for publication: The 9th IJCAR Automated Theorem Proving System Competition – CASC-J9