Isabelle/Isar
From MaRDI portal
Cited in
(only showing first 100 items - show all)- A mechanised abstract formalisation of concept lattices
- Comprehending Isabelle/HOL’s Consistency
- scientific article; zbMATH DE number 1927415 (Why is no real title available?)
- Mathematical Knowledge Management
- The seventeen provers of the world. Foreword by Dana S. Scott..
- A hierarchy of semantics for non-deterministic term rewriting systems
- Tool-Based Verification of a Relational Vertex Coloring Program
- Building Formal Method Tools in the Isabelle/Isar Framework
- Towards formalising Schutz' axioms for Minkowski spacetime in Isabelle/HOL
- Fast formal proof of the Erdős-Szekeres conjecture for convex polygons with at most 6 points
- Pervasive parallelism in highly-trustable interactive theorem proving systems
- Interpreting mathematical texts in Naproche-SAD
- Relational and Kleene-Algebraic Methods in Computer Science
- A synthesis of the procedural and declarative styles of interactive theorem proving
- Logic for Programming, Artificial Intelligence, and Reasoning
- Interactive verification of architectural design patterns in FACTum
- Automating theorem proving with SMT
- Improving legibility of formal proofs based on the close reference principle is NP-hard
- On definitions of constants and types in HOL
- A generic and executable formalization of signature-based Gröbner basis algorithms
- Formalization of the Poincaré disc model of hyperbolic geometry
- The Isabelle Framework
- Merging Procedural and Declarative Proof
- Student proof exercises using MathsTiles and Isabelle/HOL in an intelligent book
- A certified proof of the Cartan fixed point theorems
- Types for Proofs and Programs
- Automated Improving of Proof Legibility in the Mizar System
- Supporting the formal verification of mathematical texts
- KAT-ML: an interactive theorem prover for Kleene algebra with tests
- Formal Proof of the Group Law for Edwards Elliptic Curves
- Logic-Free Reasoning in Isabelle/Isar
- Verifying a Hotel Key Card System
- A UTP semantic model for Orc language with execution status and fault handling
- Local Theory Specifications in Isabelle/Isar
- Translating Scala programs to Isabelle/HOL. System description
- Tutorial to locales and locale interpretation
- Using Isabelle/HOL to verify first-order relativity theory
- scientific article; zbMATH DE number 5713654 (Why is no real title available?)
- Formalizing Bachmair and Ganzinger's ordered resolution prover
- Types for Proofs and Programs
- Shortening of proof length is elusive for theorem provers
- Types for Proofs and Programs
- Types for Proofs and Programs
- Structured Induction Proofs in Isabelle/Isar
- Mechanical Theorem Proving in Tarski’s Geometry
- Dependently-typed formalisation of relation-algebraic abstractions
- Structured formal development in Isabelle
- An efficient Coq tactic for deciding Kleene algebras
- Jinja: towards a comprehensive formal semantics for a Java-like language
- The formalization of Vickrey auctions: a comparison of two approaches in Isabelle and Theorema
- Relational characterisations of paths
- Formalization of Dubé's degree bounds for Gröbner bases in Isabelle/HOL
- Mathematical method and proof
- Type classes and filters for mathematical analysis in Isabelle/HOL
- Isabelle
- TkWinHOL
- Rapide
- MizarMode
- Isar
- Proof General
- Isabelle/ZF
- TAS
- HOL-OCL
- Saoithin
- Isabelle/jEdit
- PIDE
- UTP2
- Isabelle/PIDE
- MathBrush
- KAT-ML
- RALL
- ForMaRE
- EAT
- jEdit
- iJulienne
- PhoX
- ProofWeb
- Poly/ML
- FoCaLiZe
- Locales
- Eisbach
- Metamath
- RATH-Agda
- CC-Pi
- Xtext
- PolyML
- miz3
- XBarnacle
- Lifting
- ltl2dstar
- Transfer
- WorkflowFM
- UTPCalc
- MMode
- SWT
- Cayley-Hamilton
- Archive Formal Proofs
- ATBR
- Arrow Gibbard Satterthwaite
- Depth First Search
This page was built for software: Isabelle/Isar
