The following pages link to HOL Light (Q18672):
Displaying 50 items.
- The future of logic: foundation-independence (Q263104) (← links)
- The reflective Milawa theorem prover is sound (down to the machine code that runs it) (Q286790) (← links)
- Formal proofs of hypergeometric sums. Dedicated to the memory of Andrzej Trybulec (Q286798) (← links)
- MizAR 40 for Mizar 40 (Q286800) (← links)
- The higher-order prover \textsc{Leo}-II (Q287283) (← links)
- On definitions of constants and types in HOL (Q287358) (← links)
- Self-formalisation of higher-order logic. Semantics, soundness, and a verified implementation (Q287361) (← links)
- A heuristic prover for real inequalities (Q287379) (← links)
- On the formal analysis of Gaussian optical systems in HOL (Q315313) (← links)
- A learning-based fact selector for Isabelle/HOL (Q331617) (← links)
- Floating-point arithmetic on the test bench. How are verified numerical solutions calculated? (Q335016) (← links)
- Intelligent computer mathematics. MKM, Calculemus, DML, and systems and projects 2013, held as part of CICM 2013, Bath, UK, July 8--12, 2013. Proceedings (Q352758) (← links)
- Proceedings of the 3rd workshop on pragmatics of decision procedures in automated reasoning (PDPAR 2005), Edinburgh, UK, July12, 2005 (Q368046) (← links)
- Logic for programming, artificial intelligence, and reasoning. 19th international conference, LPAR-19, Stellenbosch, South Africa, December 14--19, 2013. Proceedings (Q383830) (← links)
- A condensed semantics for qualitative spatial reasoning about oriented straight line segments (Q420800) (← links)
- Combining decision procedures by (model-)equality propagation (Q436376) (← links)
- A certified proof of the Cartan fixed point theorems (Q438546) (← links)
- Monotonicity inference for higher-order formulas (Q438558) (← links)
- Analytic tableaux for higher-order logic with choice (Q438561) (← links)
- Formal analysis of optical systems (Q475384) (← links)
- Deciding floating-point logic with abstract conflict driven clause learning (Q479837) (← links)
- Learning-assisted theorem proving with millions of lemmas (Q485842) (← links)
- Efficient and accurate computation of upper bounds of approximation errors (Q633637) (← links)
- Representing model theory in a type-theoretical logical framework (Q654913) (← links)
- Fast formal proof of the Erdős-Szekeres conjecture for convex polygons with at most 6 points (Q670696) (← links)
- A formalization of metric spaces in HOL Light (Q682381) (← links)
- Logic for programming, artificial intelligence, and reasoning. 17th international conference, LPAR-17, Yogyakarta, Indonesia, October 10--15, 2010. Proceedings (Q708446) (← links)
- Continuous KAOS, ASM, and formal control system design across the continuous/discrete modeling interface: a simple train stopping application (Q736916) (← links)
- Implementing geometric algebra products with binary trees (Q742367) (← links)
- On QE algorithms over an algebraically closed field based on comprehensive Gröbner systems (Q748755) (← links)
- Formal verification of the VAMP floating point unit (Q816201) (← links)
- Formalization of fixed-point arithmetic in HOL (Q816219) (← links)
- Formalization of camera pose estimation algorithm based on Rodrigues formula (Q826358) (← links)
- JEFL: joint embedding of formal proof libraries (Q831932) (← links)
- Theorem proving in higher order logics. 22nd international conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings (Q834373) (← links)
- Is ZF a hack? Comparing the complexity of some (formalist interpretations of) foundational systems for mathematics (Q865658) (← links)
- Logic for programming, artificial intelligence, and reasoning. 20th international conference, LPAR-20 2015, Suva, Fiji, November 24--28, 2015. Proceedings (Q894690) (← links)
- Selected papers based on the presentations at the 7th and 8th international workshops on numerical software verification (NSV), Vienna, Austria, July 17--18, 2014 and April 13, 2015 (Q896457) (← links)
- The higher-order-logic Formath (Q935562) (← links)
- Modules over monads and initial semantics (Q964503) (← links)
- Partial and nested recursive function definitions in higher-order logic (Q972425) (← links)
- A revision of the proof of the Kepler conjecture (Q977177) (← links)
- Interactive theorem proving. First international conference, ITP 2010, Edinburgh, UK, July 11--14, 2010. Proceedings (Q983522) (← links)
- Efficiently checking propositional refutations in HOL theorem provers (Q1006729) (← links)
- Operating system verification---an overview (Q1040002) (← links)
- Data compression for proof replay (Q1040776) (← links)
- A Skeptic's approach to combining HOL and Maple (Q1272607) (← links)
- Formal analysis of continuous-time systems using Fourier transform (Q1640640) (← links)
- Aligning concepts across proof assistant libraries (Q1640642) (← links)
- Distant decimals of \(\pi \): formal proofs of some algorithms computing them and guarantees of exact computation (Q1663216) (← links)
