The 9th IJCAR automated theorem proving system competition -- CASC-J9

DOI10.3233/AIC-180773zbMATH Open1462.68220OpenAlexW4249545655MaRDI QIDQ5145447FDOQ5145447

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

Recommendations

• The 7th IJCAR automated theorem proving system competition -- CASC-J7
• The 8th IJCAR automated theorem proving system competition -- CASC-J8
• The 10th IJCAR automated theorem proving system competition -- CASC-J10
• The CADE-22 automated theorem proving system competition -- CASC-22
• scientific article; zbMATH DE number 5305114

zbMATH Keywords

competitionautomated theorem proving

Mathematics Subject Classification ID

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

Cites Work

• The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
• nanoCoP: A Non-clausal Connection Prover
• Evaluating general purpose automated theorem proving systems
• CakeML
• Critical pair criteria for completion
• A Non-clausal Connection Calculus
• Ordered rewriting and confluence
• 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
• Non-clausal connection calculi for non-classical logics
• Selecting the Selection
• Unification with abstraction and theory instantiation in saturation-based reasoning
• Blocked Clauses in First-Order Logic
• The CADE-26 automated theorem proving system competition – CASC-26

Cited In (7)

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

Uses Software

• TPTP
• CakeML
• StarExec
• nanoCoP

This page was built for publication: The 9th IJCAR automated theorem proving system competition -- CASC-J9

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