The following pages link to (Q5287513):
Displayed 50 items.
- ML (Q13958) (← links)
- The higher-order prover \textsc{Leo}-II (Q287283) (← links)
- Semi-intelligible Isar proofs from machine-generated proofs (Q287340) (← links)
- A two-valued logic for properties of strict functional programs allowing partial functions (Q352946) (← links)
- An approach for lifetime reliability analysis using theorem proving (Q386029) (← links)
- A mechanisation of some context-free language theory in HOL4 (Q386032) (← links)
- A scalable module system (Q391632) (← links)
- Unifying sets and programs via dependent types (Q408534) (← links)
- Mechanised wire-wise verification of Handel-C synthesis (Q436367) (← links)
- Combining decision procedures by (model-)equality propagation (Q436376) (← 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)
- 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)
- Term rewriting and Hoare logic -- Coded rewriting (Q673226) (← 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)
- 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)
- Computer supported mathematics with \(\Omega\)MEGA (Q865650) (← links)
- SAD as a mathematical assistant -- how should we go from here to there? (Q865654) (← links)
- Providing a formal linkage between MDG and HOL (Q878110) (← links)
- A few exercises in theorem processing (Q879370) (← links)
- A complete axiom system for propositional projection temporal logic with cylinder computation model (Q896162) (← links)
- Formal probabilistic analysis of detection properties in wireless sensor networks (Q903510) (← links)
- A mechanical analysis of program verification strategies (Q928673) (← links)
- Proof synthesis and reflection for linear arithmetic (Q945055) (← links)
- The seven virtues of simple type theory (Q946569) (← links)
- Curry-Howard for incomplete first-order logic derivations using one-and-a-half level terms (Q964000) (← links)
- Partial and nested recursive function definitions in higher-order logic (Q972425) (← links)
- The proof monad (Q974136) (← links)
- Formalization of the standard uniform random variable (Q995466) (← links)
- Integrating external deduction tools with ACL2 (Q1006728) (← links)
- Efficiently checking propositional refutations in HOL theorem provers (Q1006729) (← links)
- Adapting functional programs to higher order logic (Q1029815) (← links)
- Proof assistants: history, ideas and future (Q1040001) (← links)
- Data compression for proof replay (Q1040776) (← links)