The 10th IJCAR automated theorem proving system competition -- CASC-J10

DOI10.3233/AIC-201566MaRDI QIDQ5019796zbMATH OpenOpenAlexFDO

Authors Geoff Sutcliffe

Publication date 11 January 2022

Published in AI Communications (Search for Journal in Brave)

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

zbMATH Keywords

automated theorem provingcompetition

Mathematics Subject Classification ID

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

Recommendations

• The 8th IJCAR automated theorem proving system competition -- CASC-J8
• The 7th IJCAR automated theorem proving system competition -- CASC-J7
• The 9th IJCAR automated theorem proving system competition -- CASC-J9
• scientific article; zbMATH DE number 5305114
• The CADE-25 automated theorem proving system competition -- CASC-25

Cites work

• A Brief Overview of HOL4
• A combinator-based superposition calculus for higher-order logic
• A Knuth-Bendix-like ordering for orienting combinator equations
• Combining proverif and automated theorem provers for security protocol verification
• Connection tableaux with lazy paramodulation
• Deciding simple infinity axiom sets with one binary relation by means of superpostulates
• Detecting inconsistencies in large first-order knowledge bases
• ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (System Description)
• ENIGMA-NG: efficient neural and gradient-boosted inference guidance for \(\mathrm{E}\)
• Evaluating general purpose automated theorem proving systems
• GRUNGE: a grand unified ATP challenge
• Hammering towards QED
• Hierarchical invention of theorem proving strategies
• scientific article; zbMATH DE number 1809862 (Why is no real title available?)
• Limited resource strategy in resolution theorem proving
• Premise selection for mathematics by corpus analysis and kernel methods
• Subsumption demodulation in first-order theorem proving
• Superposition with lambdas
• The CADE-16 ATP system competition
• The CADE-26 automated theorem proving system competition -- CASC-26
• The CADE-27 automated theorem proving system competition -- CASC-27
• The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0

Cited in

(14)

• Lash 1.0 (system description)
• scientific article; zbMATH DE number 1809860 (Why is no real title available?)
• The CADE-22 automated theorem proving system competition -- CASC-22
• The 7th IJCAR automated theorem proving system competition -- CASC-J7
• The CADE-25 automated theorem proving system competition -- CASC-25
• The 8th IJCAR automated theorem proving system competition -- CASC-J8
• The CADE-28 Automated Theorem Proving System Competition – CASC-28
• The CADE-26 automated theorem proving system competition -- CASC-26
• The 9th IJCAR automated theorem proving system competition -- CASC-J9
• Making higher-order superposition work
• The 11th IJCAR automated theorem proving system competition – CASC-J11
• Extending a high-performance prover to higher-order logic
• \texttt{gym-saturation}: gymnasium environments for saturation provers (system description)
• Duper: a proof-producing superposition theorem prover for dependent type theory

Describes a project that uses

Uses Software

• MiniSat
• lazyCoP
• TPTP
• HOL
• ProVerif
• StarExec
• E Theorem Prover
• BliStrTune
• ENIGMA

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

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