swMATH2006MaRDI QIDQ14553FDOQ14553
Author name not available (Why is that?)
Official website: http://isabelle.in.tum.de/Isar/
Cited In (only showing first 100 items - show all)
- Interpreting mathematical texts in Naproche-SAD
- A synthesis of the procedural and declarative styles of interactive theorem proving
- The Isabelle Framework
- Improving legibility of formal proofs based on the close reference principle is NP-hard
- On definitions of constants and types in HOL
- KAT-ML: an interactive theorem prover for Kleene algebra with tests
- Verifying a Hotel Key Card System
- Types for Proofs and Programs
- Types for Proofs and Programs
- Shortening of proof length is elusive for theorem provers
- Structured Induction Proofs in Isabelle/Isar
- Mechanical Theorem Proving in Tarski’s Geometry
- Dependently-typed formalisation of relation-algebraic abstractions
- 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
- A formally verified proof of the central limit theorem
- miz3
- XBarnacle
- Lifting
- ltl2dstar
- Transfer
- WorkflowFM
- UTPCalc
- MMode
- SWT
- Cayley-Hamilton
- Archive Formal Proofs
- ATBR
- Arrow Gibbard Satterthwaite
- Depth First Search
- Diophantine
- Graph Theory
- PairingHeap
- Psi-calculi
- Skew Heap
- Regular Sets
- SAT Solver Verification
- Hotel Key Card
- Splay Tree
- Stable Matching
- Verified Prover
- Slicing
- Worker/Wrapper Transformation
- ProofPeer
- Dynamic Architectures
- FACTum
- XIsabelle
- FOL_Harrison
- Groebner_Bases
- GeoCoq
- Jape
- Vickrey_Clarke_Groves
- F5C
- A comparison of Mizar and Isar
- Interactive theorem proving from the perspective of Isabelle/Isar
- Naproche-SAD
- Architectural_Design_Patterns
- Psi-calculi in Isabelle
- Locales: a module system for mathematical theories
- 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
- Proviola: a tool for proof re-animation
- From Tarski to Hilbert
- Automated Reasoning in Higher-Order Regular Algebra
- An Isabelle proof method language
- A formally verified solver for homogeneous linear Diophantine equations
- Automating theorem proving with SMT
- Student proof exercises using MathsTiles and Isabelle/HOL in an intelligent book
This page was built for software: Isabelle/Isar
