The 11th IJCAR automated theorem proving system competition – CASC-J11

DOI10.3233/aic-220244WikidataQ122234818 ScholiaQ122234818MaRDI QIDQ6095787

Martin Desharnais, Geoff Sutcliffe

Publication date: 8 September 2023

Published in: AI Communications (Search for Journal in Brave)

zbMATH Keywords

competitionautomated theorem proving

Mathematics Subject Classification ID

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

Cites Work

• Unnamed Item
• Unnamed Item
• Relational lattices: from databases to universal algebra
• ATP-based cross-verification of Mizar proofs: method, systems, and first experiments
• Evaluating general purpose automated theorem proving systems
• The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0
• Generalized MV-algebras
• Efficient encodings of first-order Horn formulas in equational logic
• An abstraction-refinement framework for reasoning with large theories
• The CADE-16 ATP system competition
• Superposition for full higher-order logic
• Layered clause selection for theory reasoning (short paper)
• Ground joinability and connectedness in the superposition calculus
• Lash 1.0 (system description)
• \textsf{Goéland}: a concurrent tableau-based theorem prover (system description)
• Vampire getting noisy: Will random bits help conquer chaos? (system description)
• Heterogeneous heuristic optimisation and scheduling for first-order theorem proving
• AC simplifications and closure redundancies in the superposition calculus
• Making theory reasoning simpler
• GRUNGE: a grand unified ATP challenge
• Faster, higher, stronger: E 2.3
• Detecting inconsistencies in large first-order knowledge bases
• Automated Reasoning Service for HOL Light
• Satallax: An Automatic Higher-Order Prover
• Beagle – A Hierarchic Superposition Theorem Prover
• Playing with AVATAR
• iProver – An Instantiation-Based Theorem Prover for First-Order Logic (System Description)
• Generation and Verification of Finite Models and Counterexamples Using an Automated Theorem Prover Answering Two Open Questions
• Inst-Gen – A Modular Approach to Instantiation-Based Automated Reasoning
• Implementing Superposition in iProver (System Description)
• The CADE-28 Automated Theorem Proving System Competition – CASC-28
• Theory and Applications of Satisfiability Testing
• Detecting Unknots via Equational Reasoning, I: Exploration
• A Constraint Sequent Calculus for First-Order Logic with Linear Integer Arithmetic
• Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder
• Superposition with lambdas
• Making higher-order superposition work
• The logic languages of the TPTP world

This page was built for publication: The 11th IJCAR automated theorem proving system competition – CASC-J11