Automation of Boolos' Curious Inference in Isabelle/HOL
From MaRDI portal
- A curious inference
- A formulation of the simple theory of types.
- An introduction to mathematical logic and type theory: To truth through proof.
- Comparing approaches to resolution based higher-order theorem proving
- Don't eliminate cut
- Extensional higher-order paramodulation in Leo-III
- Faster, higher, stronger: E 2.3
- Hammering towards QED
- Unnamed Publication
- Unnamed Publication
- Unnamed Publication
- Unnamed Publication
- Unnamed Publication
- Isabelle/HOL. A proof assistant for higher-order logic
- Isabelle/jEdit – A Prover IDE within the PIDE Framework
- Knowledge-based proof planning
- Lemma discovery for induction. A survey
- Mizar: state-of-the-art and beyond
- On connections and higher-order logic
- Resource-Adaptive Cognitive Processes
- Short proofs without new variables
- Superposition with lambdas
- The higher-order prover \textsc{Leo}-II
- The higher-order prover Leo-III
- The logic languages of the TPTP world
- The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0
- Who finds the short proof?
- Zum Hilbertschen Aufbau der reellen Zahlen.
This page was built for software: Automation of Boolos' Curious Inference in Isabelle/HOL
