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

DOI10.3233/AIC-201566zbMATH Open1485.68287OpenAlexW4243308851MaRDI QIDQ5019796FDOQ5019796

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

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

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
• A Brief Overview of HOL4
• Title not available (Why is that?)
• Hierarchical invention of theorem proving strategies
• Evaluating general purpose automated theorem proving systems
• Premise selection for mathematics by corpus analysis and kernel methods
• Limited resource strategy in resolution theorem proving
• A combinator-based superposition calculus for higher-order logic
• ENIGMA-NG: efficient neural and gradient-boosted inference guidance for \(\mathrm{E}\)
• ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (System Description)
• Hammering towards QED
• Superposition with lambdas
• Connection tableaux with lazy paramodulation
• Subsumption demodulation in first-order theorem proving
• The CADE-16 ATP system competition
• The CADE-27 automated theorem proving system competition -- CASC-27
• Deciding simple infinity axiom sets with one binary relation by means of superpostulates
• A Knuth-Bendix-like ordering for orienting combinator equations
• GRUNGE: a grand unified ATP challenge
• Detecting inconsistencies in large first-order knowledge bases
• Combining proverif and automated theorem provers for security protocol verification
• The CADE-26 automated theorem proving system competition -- CASC-26

Cited In (13)

• Lash 1.0 (system description)
• The CADE-26 automated theorem proving system competition -- CASC-26
• Title not available (Why is that?)
• The CADE-25 automated theorem proving system competition -- CASC-25
• The 7th IJCAR automated theorem proving system competition -- CASC-J7
• The 8th IJCAR automated theorem proving system competition -- CASC-J8
• The CADE-22 automated theorem proving system competition -- CASC-22
• Making higher-order superposition work
• The CADE-28 Automated Theorem Proving System Competition – CASC-28
• The 9th IJCAR automated theorem proving system competition -- CASC-J9
• 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)

Uses Software

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

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)