The 11th IJCAR automated theorem proving system competition

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