scientific article; zbMATH DE number 234014
From MaRDI portal
Publication:5287513
Recommendations
Cited in
(only showing first 100 items - show all)- Integrating external deduction tools with ACL2
- Efficiently checking propositional refutations in HOL theorem provers
- Adapting functional programs to higher order logic
- Proof assistants: history, ideas and future
- Data compression for proof replay
- Using theorem proving to verify expectation and variance for discrete random variables
- Higher-order rewrite systems and their confluence
- Theories for mechanical proofs of imperative programs
- Formal verification of a programming logic for a distributed programming language
- The \(HOL\) logic extended with quantification over type variables
- Lazy techniques for fully expansive theorem proving
- An exercise in the automatic verification of asynchronous designs
- ML
- A linear logical framework
- A rewriting approach to satisfiability procedures.
- Algebraic models of correctness for abstract pipelines.
- The calculus of constructions as a framework for proof search with set variable instantiation
- Deductive verification of real-time systems using STeP
- Isabelle/HOL. A proof assistant for higher-order logic
- Proof assistance for real-time systems using an interactive theorem prover
- Evaluating general purpose automated theorem proving systems
- On the desirability of mechanizing calculational proofs
- Formal analysis of the kinematic Jacobian in screw theory
- A theory of formal synthesis via inductive learning
- From types to sets by local type definition in higher-order logic
- A consistent foundation for Isabelle/HOL
- Incorporating quotation and evaluation into Church's type theory
- Organizing numerical theories using axiomatic type classes
- A UTP semantics for communicating processes with shared variables and its formal encoding in PVS
- Structuring metatheory on inductive definitions
- Weakest pre-condition reasoning for Java programs with JML annotations
- Interpreting HOL in the calculus of constructions
- Secure mechanical verification of mutually recursive procedures
- An approach to literate and structured formal developments
- TPS: A theorem-proving system for classical type theory
- N. G. de Bruijn (1918--2012) and his road to Automath, the earliest proof checker
- Unifying theories in ProofPower-Z
- Superposition for full higher-order logic
- The role of entropy in guiding a connection prover
- Joshua Guttman: pioneering strand spaces
- Program logic for higher-order probabilistic programs in Isabelle/HOL
- CryptHOL: game-based proofs in higher-order logic
- Unique solutions of contractions, CCS, and their HOL formalisation
- From LCF to Isabelle/HOL
- Milestones from the Pure Lisp Theorem Prover to ACL2
- Limited second-order functionality in a first-order setting
- GRUNGE: a grand unified ATP challenge
- Mechanized metatheory revisited
- Formalization of geometric algebra in HOL Light
- A framework for the verification of certifying computations
- Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
- On the formalization of gamma function in HOL
- Soundness and completeness proofs by coinductive methods
- Theory morphisms in Church's type theory with quotation and evaluation
- Verifying a scheduling protocol of safety-critical systems
- Automation for interactive proof: first prototype
- Formal reasoning about finite-state discrete-time Markov chains in HOL
- Dealing with algebraic expressions over a field in Coq using Maple
- An approach to formal verification of human-computer interaction
- Translating higher-order clauses to first-order clauses
- Error analysis of digital filters using HOL theorem proving
- Semantic essence of AsmL
- Probabilistic guarded commands mechanized in HOL
- A decision procedure for linear ``big O equations
- Mechanizing common knowledge logic using COQ
- Computer assisted reasoning. A Festschrift for Michael J. C. Gordon
- Formalizing an analytic proof of the prime number theorem
- Rewriting conversions implemented with continuations
- Extensional higher-order paramodulation in Leo-III
- Automated reasoning for probabilistic sequential programs with theorem proving
- scientific article; zbMATH DE number 1617310 (Why is no real title available?)
- scientific article; zbMATH DE number 1670733 (Why is no real title available?)
- Incorporating quotation and evaluation into Church's type theory: syntax and semantics
- HOL Zero's solutions for Pollack-inconsistency
- From types to sets by local type definitions in higher-order logic
- Programmed strategies for program verification
- A logical framework with explicit conversions
- The higher-order prover \textsc{Leo}-II
- Semi-intelligible Isar proofs from machine-generated proofs
- A compiled implementation of normalisation by evaluation
- Auto in Agda. Programming proof search using reflection
- A consistent foundation for Isabelle/HOL
- Friends with benefits. Implementing corecursion in foundational proof assistants
- Comprehending Isabelle/HOL’s Consistency
- scientific article; zbMATH DE number 2185697 (Why is no real title available?)
- Formalization of entropy measures in HOL
- Automatic proof and disproof in Isabelle/HOL
- Combining Model Checking and Deduction
- Symbolic trajectory evaluation
- Without Loss of Generality
- HOL Light: An Overview
- Formal Analysis of Optical Waveguides in HOL
- The HOL-Omega Logic
- Machine-checked proof-theory for propositional modal logics
- A two-valued logic for properties of strict functional programs allowing partial functions
- LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description)
- THF0 – The Core of the TPTP Language for Higher-Order Logic
- Twenty Years of Theorem Proving for HOLs Past, Present and Future
- A Brief Overview of HOL4
- A Compiled Implementation of Normalization by Evaluation
This page was built for publication:
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5287513)
