The 11th IJCAR automated theorem proving system competition – CASC-J11
From MaRDI portal
Publication:6095787
DOI10.3233/aic-220244WikidataQ122234818 ScholiaQ122234818MaRDI QIDQ6095787
Martin Desharnais, Geoff Sutcliffe
Publication date: 8 September 2023
Published in: AI Communications (Search for Journal in Brave)
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