The following pages link to HOL (Q17631):
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)
- Improving legibility of formal proofs based on the close reference principle is NP-hard (Q286805) (← links)
- The higher-order prover \textsc{Leo}-II (Q287283) (← links)
- Semi-intelligible Isar proofs from machine-generated proofs (Q287340) (← links)
- Interactive theorem proving. Preface of the special issue (Q287356) (← 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)
- Formalization of reliability block diagrams in higher-order logic (Q334147) (← links)
- A two-valued logic for properties of strict functional programs allowing partial functions (Q352946) (← links)
- Wu's characteristic set method for SystemVerilog assertions verification (Q364509) (← links)
- An approach for lifetime reliability analysis using theorem proving (Q386029) (← links)
- A mechanisation of some context-free language theory in HOL4 (Q386032) (← links)
- Programming and automating mathematics in the Tarski-Kleene hierarchy (Q406433) (← links)
- Unifying sets and programs via dependent types (Q408534) (← links)
- Mechanised wire-wise verification of Handel-C synthesis (Q436367) (← links)
- Function extraction (Q436372) (← links)
- Monotonicity inference for higher-order formulas (Q438558) (← links)
- Analytic tableaux for higher-order logic with choice (Q438561) (← links)
- Automatic verification of reduction techniques in higher order logic (Q469363) (← links)
- An inductive approach to strand spaces (Q470008) (← links)
- Formal analysis of optical systems (Q475384) (← links)
- The right tools for the job: correctness of cone of influence reduction proved using ACL2 and HOL4 (Q540690) (← links)
- Reasoning about conditional probabilities in a higher-order-logic theorem prover (Q545151) (← links)
- Formal reliability analysis of combinational circuits using theorem proving (Q545153) (← links)
- Structured derivations: a unified proof style for teaching mathematics (Q607406) (← links)
- Tactics for hierarchical proof (Q626933) (← 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)
- Amortized complexity verified (Q670702) (← links)
- Term rewriting and Hoare logic -- Coded rewriting (Q673226) (← links)
- Verification of a multiprocessor cache protocol using simulation relations and higher-order logic (Q685110) (← links)
- Specification and automatic verification of self-timed queues (Q685115) (← links)
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring. (Q703860) (← links)
- Validating the PSL/Sugar semantics using automated reasoning (Q706502) (← links)
- Continuous KAOS, ASM, and formal control system design across the continuous/discrete modeling interface: a simple train stopping application (Q736916) (← links)
- N. G. de Bruijn's contribution to the formalization of mathematics (Q740481) (← links)
- Implementing geometric algebra products with binary trees (Q742367) (← links)
- Generalization in the presence of free variables: A mechanically-checked correctness proof for one algorithm (Q757074) (← links)
- Formal reliability and failure analysis of Ethernet based communication networks in a smart grid substation (Q782499) (← links)
- Logic-based subsumption architecture (Q814558) (← links)
- A complete mechanization of correctness of a string-preprocessing algorithm (Q816208) (← links)
- Two case studies of semantics execution in Maude: CCS and LOTOS (Q816216) (← links)
- Formalization of fixed-point arithmetic in HOL (Q816219) (← links)
- Proof pearl: Mechanizing the textbook proof of Huffman's algorithm (Q839031) (← links)
- Simplifying proofs in Fitch-style natural deduction systems (Q851139) (← links)
- Ordinal arithmetic: Algorithms and mechanization (Q851144) (← links)
- Deciding Boolean algebra with Presburger arithmetic (Q861705) (← links)
- TPS: A hybrid automatic-interactive system for developing proofs (Q865629) (← links)
- A proof-centric approach to mathematical assistants (Q865648) (← links)
