Isabelle/Isar

swMATH2006MaRDI QIDQ14553FDOQ14553

Author name not available (Why is that?)

Cited In (98)

• Building Formal Method Tools in the Isabelle/Isar Framework
• Towards formalising Schutz' axioms for Minkowski spacetime in Isabelle/HOL
• Merging Procedural and Declarative Proof
• Student proof exercises using MathsTiles and Isabelle/HOL in an intelligent book
• Types for Proofs and Programs
• Logic-Free Reasoning in Isabelle/Isar
• The formalization of Vickrey auctions: a comparison of two approaches in Isabelle and Theorema
• Formalization of Dubé's degree bounds for Gröbner bases in Isabelle/HOL
• Translating Scala Programs to Isabelle/HOL
• Formalizing a Framework for Dynamic Slicing of Program Dependence Graphs in Isabelle/HOL
• Managing Proof Documents for Asynchronous Processing
• Interactive Simplifier Tracing and Debugging in Isabelle
• UTPCalc — A Calculator for UTP Predicates
• Correctness of Pointer Manipulating Algorithms Illustrated by a Verified BDD Construction
• Understanding and maintaining tactics graphically OR how we are learning that a diagram can be worth more than 10K LoC
• Semantics of Mizar as an Isabelle object logic
• Modelling algebraic structures and morphisms in ACL2
• Automating Theorem Proving with SMT
• Mathematical Knowledge Management
• The seventeen provers of the world. Foreword by Dana S. Scott..
• Tool-Based Verification of a Relational Vertex Coloring Program
• Title not available (Why is that?)
• Title not available (Why is that?)
• Fast formal proof of the Erdős-Szekeres conjecture for convex polygons with at most 6 points
• Interpreting mathematical texts in Naproche-SAD
• Relational and Kleene-Algebraic Methods in Computer Science
• Type Classes and Filters for Mathematical Analysis in Isabelle/HOL
• An Efficient Coq Tactic for Deciding Kleene Algebras
• An Isabelle Proof Method Language
• Logic for Programming, Artificial Intelligence, and Reasoning
• A synthesis of the procedural and declarative styles of interactive theorem proving
• Interactive verification of architectural design patterns in FACTum
• Title not available (Why is that?)
• The Isabelle Framework
• A generic and executable formalization of signature-based Gröbner basis algorithms
• Formalization of the Poincaré disc model of hyperbolic geometry
• Improving legibility of formal proofs based on the close reference principle is NP-hard
• On definitions of constants and types in HOL
• Proviola: A Tool for Proof Re-animation
• Automated Improving of Proof Legibility in the Mizar System
• Formal Proof of the Group Law for Edwards Elliptic Curves
• A certified proof of the Cartan fixed point theorems
• KAT-ML: an interactive theorem prover for Kleene algebra with tests
• Verifying a Hotel Key Card System
• Supporting the formal verification of mathematical texts
• Local Theory Specifications in Isabelle/Isar
• A Hierarchy of Semantics for Non-deterministic Term Rewriting Systems ∗
• A UTP semantic model for Orc language with execution status and fault handling
• Pervasive Parallelism in Highly-Trustable Interactive Theorem Proving Systems
• Formalizing Bachmair and Ganzinger's ordered resolution prover
• Types for Proofs and Programs
• Types for Proofs and Programs
• Types for Proofs and Programs
• Using Isabelle/HOL to verify first-order relativity theory
• Title not available (Why is that?)
• Structured Induction Proofs in Isabelle/Isar
• Mechanical Theorem Proving in Tarski’s Geometry
• Relational characterisations of paths
• Mathematical method and proof
• Test-Sequence Generation with Hol-TestGen with an Application to Firewall Testing
• Theorem Proving in Higher Order Logics
• Numerical Analysis of Ordinary Differential Equations in Isabelle/HOL
• Refinement-Based Verification of Interactive Real-Time Systems
• A formally verified proof of the central limit theorem
• Verified interactive computation of definite integrals
• Towards verified handwritten calculational proofs (short paper)
• Towards formal foundations for game theory
• A comparison of Mizar and Isar
• A Vernacular for Coherent Logic
• Theories as types
• A Mechanised Abstract Formalisation of Concept Lattices
• A mechanized proof of the basic perturbation lemma
• From LCF to Isabelle/HOL
• Interaction with formal mathematical documents in Isabelle/PIDE
• Dependently-Typed Formalisation of Relation-Algebraic Abstractions
• Title not available (Why is that?)
• Psi-calculi in Isabelle
• Locales: a module system for mathematical theories
• Proving pointer programs in higher-order logic
• Programming and verifying a declarative first-order prover in Isabelle/HOL
• Constructive Type Classes in Isabelle
• A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality
• Title not available (Why is that?)
• From LTL to deterministic automata. A safraless compositional approach
• Partial and nested recursive function definitions in higher-order logic
• Interactive Proving, Higher-Order Rewriting, and Theory Analysis in Theorema 2.0
• Improving legibility of natural deduction proofs is not trivial
• From Tarski to Hilbert
• Automated Reasoning in Higher-Order Regular Algebra
• Interpretation of Locales in Isabelle: Theories and Proof Contexts
• Automation for interactive proof: first prototype
• Amortized complexity verified
• A formally verified solver for homogeneous linear Diophantine equations
• Shortening of Proof Length is Elusive for Theorem Provers
• A consistent foundation for Isabelle/HOL
• Title not available (Why is that?)
• Comprehending Isabelle/HOL’s Consistency
• Title not available (Why is that?)

This page was built for software: Isabelle/Isar