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

DOI10.3233/AIC-180773MaRDI QIDQ5145447zbMATH OpenOpenAlexFDO

Authors 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)

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

Cites work

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

Cited in

(11)

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

Describes a project that uses

Uses Software

• nanoCoP
• StarExec
• CakeML
• TPTP

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)