Isabelle/HOL. A proof assistant for higher-order logic
From MaRDI portal
Publication:1600086
zbMath0994.68131MaRDI QIDQ1600086
Tobias Nipkow, Markus Wenzel, Lawrence Charles Paulson
Publication date: 12 June 2002
Published in: Lecture Notes in Computer Science (Search for Journal in Brave)
Mechanization of proofs and logical operations (03B35) Research exposition (monographs, survey articles) pertaining to computer science (68-02)
Related Items (only showing first 100 items - show all)
Concurrent Dynamic Algebra ⋮ An Assertional Proof of the Stability and Correctness of Natural Mergesort ⋮ Convolution as a Unifying Concept ⋮ Taming Multirelations ⋮ How Hard Is Positive Quantification? ⋮ Survey on Parameterized Verification with Threshold Automata and the Byzantine Model Checker ⋮ A FORMAL PROOF OF THE KEPLER CONJECTURE ⋮ Stone Relation Algebras ⋮ Reasoning About Cardinalities of Relations with Applications Supported by Proof Assistants ⋮ Unnamed Item ⋮ Automated Kantian ethics: a faithful implementation ⋮ Specification and verification of concurrent systems by causality and realizability ⋮ Fundamentals of compositional rewriting theory ⋮ Mechanical certification of \(\mathrm{FOL_{ID}}\) cyclic proofs ⋮ Analysis and Transformation of Constrained Horn Clauses for Program Verification ⋮ A formalised theorem in the partition calculus ⋮ The MET: The Art of Flexible Reasoning with Modalities ⋮ A Formal Proof of the Computation of Hermite Normal Form in a General Setting ⋮ Into the Infinite - Theory Exploration for Coinduction ⋮ Machine Learning for Inductive Theorem Proving ⋮ VeriMon: a formally verified monitoring tool ⋮ Rensets and renaming-based recursion for syntax with bindings extended version ⋮ Embedded domain specific verifiers ⋮ What is the point of computers? A question for pure mathematicians ⋮ Isabelle formalisation of original representation theorems ⋮ SAT-Inspired Higher-Order Eliminations ⋮ Formalising Szemerédi's Regularity Lemma and Roth's Theorem on Arithmetic Progressions in Isabelle/HOL ⋮ Wetzel: formalisation of an undecidable problem linked to the continuum hypothesis ⋮ Combining higher-order logic with set theory formalizations ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ \textsf{symQV}: automated symbolic verification of quantum programs ⋮ A fine-grained semantics for arrays and pointers under weak memory models ⋮ Verifying feedforward neural networks for classification in Isabelle/HOL ⋮ Integrating ADTs in KeY and their application to history-based reasoning about collection ⋮ Verified verifying: SMT-LIB for strings in Isabelle ⋮ Verified decision procedures for MSO on words based on derivatives of regular expressions ⋮ Formalisation in higher-order logic and code generation to functional languages of the Gauss-Jordan algorithm ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Formal power series ⋮ Higher-Order Tarski Grothendieck as a Foundation for Formal Proof. ⋮ Binary-Compatible Verification of Filesystems with ACL2 ⋮ Refinement-Based Verification of Interactive Real-Time Systems ⋮ Experimenting Formal Proofs of Petri Nets Refinements ⋮ Reasoning About Multi-Lingual Exception Handling Using RIPLS ⋮ Analogy in Automated Deduction: A Survey ⋮ CSP-CASL-Prover: A Generic Tool for Process and Data Refinement ⋮ The Stable Revivals Model in CSP-Prover ⋮ A Flexible Framework for Visualisation of Computational Properties of General Explicit Substitutions Calculi ⋮ A Theoretical Framework for the Higher-Order Cooperation of Numeric Constraint Domains ⋮ Formal Verification of Graph Grammars using Mathematical Induction ⋮ Verified Compilation and the B Method: A Proposal and a First Appraisal ⋮ Combining Decision Procedures by (Model-)Equality Propagation ⋮ A case-study in algebraic manipulation using mechanized reasoning tools ⋮ Binary codes that do not preserve primitivity ⋮ Progress in the Development of Automated Theorem Proving for Higher-Order Logic ⋮ Calculational relation-algebraic proofs in the teaching tool \textsc{CalcCheck} ⋮ A formal proof of the expressiveness of deep learning ⋮ Extending Sledgehammer with SMT Solvers ⋮ Heaps and Data Structures: A Challenge for Automated Provers ⋮ A Formalization of the C99 Standard in HOL, Isabelle and Coq ⋮ Verified analysis of random binary tree structures ⋮ Formalizing Bachmair and Ganzinger's ordered resolution prover ⋮ Cardinality of relations and relational approximation algorithms ⋮ Using First-Order Theorem Provers in the Jahob Data Structure Verification System ⋮ Decision Procedures for Multisets with Cardinality Constraints ⋮ The problem of proof identity, and why computer scientists should care about Hilbert's 24th problem ⋮ Certified Reasoning with Infinity ⋮ A comprehensive framework for saturation theorem proving ⋮ Reconstructor: a computer program that uses three-valued logics to represent lack of information in empirical scientific contexts ⋮ Scalable fine-grained proofs for formula processing ⋮ Efficient verified (UN)SAT certificate checking ⋮ MECHANIZING PRINCIPIA LOGICO-METAPHYSICA IN FUNCTIONAL TYPE-THEORY ⋮ Set Theory or Higher Order Logic to Represent Auction Concepts in Isabelle? ⋮ On Correctness of Mathematical Texts from a Logical and Practical Point of View ⋮ Formalizing Scientifically Applicable Mathematics in a Definitional Framework ⋮ Proof Auditing Formalised Mathematics ⋮ A comprehensive framework for saturation theorem proving ⋮ Compositional Assume-Guarantee Reasoning of Control Law Diagrams Using UTP ⋮ Free Theorems and Runtime Type Representations ⋮ Verifying safety properties of a nonlinear control by interactive theorem proving with the prototype verification system ⋮ A mechanised proof of Gödel's incompleteness theorems using Nominal Isabelle ⋮ The reflective Milawa theorem prover is sound (down to the machine code that runs it) ⋮ Mechanizing complemented lattices within Mizar type system ⋮ The higher-order prover \textsc{Leo}-II ⋮ Semi-intelligible Isar proofs from machine-generated proofs ⋮ Eisbach: a proof method language for Isabelle ⋮ Mechanizing a process algebra for network protocols ⋮ A heuristic prover for real inequalities ⋮ A Datalog hammer for supervisor verification conditions modulo simple linear arithmetic ⋮ CoqQFBV: a scalable certified SMT quantifier-free bit-vector solver ⋮ Proving fairness and implementation correctness of a microkernel scheduler
Uses Software
This page was built for publication: Isabelle/HOL. A proof assistant for higher-order logic
