Isar

swMATH4599MaRDI QIDQ16770FDOQ16770

Author name not available (Why is that?)

Cited In (only showing first 100 items - show all)

• A hierarchy of semantics for non-deterministic term rewriting systems
• Liveness Reasoning with Isabelle/HOL
• Building Formal Method Tools in the Isabelle/Isar Framework
• Towards formalising Schutz' axioms for Minkowski spacetime in Isabelle/HOL
• Towards Formal Proof Script Refactoring
• Specifying properties of dynamic architectures using configuration traces
• First steps towards a formalization of forcing
• A user interface for a mathematical system that allows ambiguous formulae
• Formal Proof: Reconciling Correctness and Understanding
• Interactive verification of architectural design patterns in FACTum
• A generic and executable formalization of signature-based Gröbner basis algorithms
• Merging Procedural and Declarative Proof
• Student proof exercises using MathsTiles and Isabelle/HOL in an intelligent book
• Automated Improving of Proof Legibility in the Mizar System
• A tactic language for declarative proofs
• Logic-Free Reasoning in Isabelle/Isar
• Formal Proof of the Group Law for Edwards Elliptic Curves
• Title not available (Why is that?)
• Implementing Spi Calculus Using Nominal Techniques
• A UTP semantic model for Orc language with execution status and fault handling
• A Modular Type Reconstruction Algorithm
• Tutorial to locales and locale interpretation
• From informal to formal proofs in Euclidean geometry
• Declarative Proof Translation (Short Paper)
• Stochastic Schrödinger equation for a quantum oscillator with dissipation
• The formalization of Vickrey auctions: a comparison of two approaches in Isabelle and Theorema
• Verified analysis of random binary tree structures
• Relational characterisations of paths
• Declarative representation of proof terms
• Crystal: Integrating structured queries into a tactic language
• Semantics, calculi, and analysis for object-oriented specifications
• A verified SAT solver framework with learn, forget, restart, and incrementality
• CoSMed: a confidentiality-verified social media platform
• Premise selection in the Naproche system
• Teaching semantics with a proof assistant: no more LSD trip proofs
• Authoring Verified Documents by Interactive Proof Construction and Verification in Text-Editors
• Refinement-Based Verification of Interactive Real-Time Systems
• Bridging the gap between argumentation theory and the philosophy of mathematics
• Accessing the Mizar library with a weakly strict Mizar parser
• Automated generation of machine verifiable and readable proofs: a case study of Tarski's geometry
• Formalizing complex plane geometry
• Tinycals: step by step tacticals
• Proof assistants: history, ideas and future
• From LCF to Isabelle/HOL
• Formalising the pi-calculus using nominal logic
• Translating between language and logic: what is easy and what is difficult
• Foundational (co)datatypes and (co)recursion for higher-order logic
• Programming and verifying a declarative first-order prover in Isabelle/HOL
• UTPCalc -- a calculator for UTP predicates
• Semantics of Mizar as an Isabelle object logic
• From LTL to deterministic automata. A safraless compositional approach
• Second-order properties of undirected graphs
• A vernacular for coherent logic
• Formalizing provable anonymity in Isabelle/HOL
• Comprehending Isabelle/HOL’s Consistency
• Verified lightweight bytecode verification
• The seventeen provers of the world. Foreword by Dana S. Scott..
• Flyspeck II: The basic linear programs
• A graphical user interface for formal proofs in geometry
• Title not available (Why is that?)
• Faster and more complete extended static checking for the Java modeling language
• HOL-Boogie -- an interactive prover-backend for the verifying C compiler
• \textsc{Plat}{\(\Omega\)}: a mediator between text-editors and proof assistance systems
• Balancing the load. Leveraging a semantics stack for systems verification
• ATP-based cross-verification of Mizar proofs: method, systems, and first experiments
• An intuitionistic proof of a discrete form of the Jordan curve theorem formalized in Coq with combinatorial hypermaps
• A synthesis of the procedural and declarative styles of interactive theorem proving
• A Brief Overview of Mizar
• Formalization of the resolution calculus for first-order logic
• 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
• Semi-intelligible Isar proofs from machine-generated proofs
• Mathematical Knowledge Management
• Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax
• Extending MKM formats at the statement level
• A proof-centric approach to mathematical assistants
• Supporting the formal verification of mathematical texts
• Local Theory Specifications in Isabelle/Isar
• Using Isabelle/HOL to verify first-order relativity theory
• Title not available (Why is that?)
• Shortening of proof length is elusive for theorem provers
• Master-equations for the study of decoherence
• Structured Induction Proofs in Isabelle/Isar
• Computer theorem proving in mathematics
• Barendregt’s Variable Convention in Rule Inductions
• Fractional generalization of the quantum Markovian master equation
• Structured derivations: a unified proof style for teaching mathematics
• Quantum non-Markovian stochastic equations
• Set graphs. III: Proof pearl: Claw-free graphs mirrored into transitive hereditarily finite sets
• Mathematical method and proof
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• An inductive approach to strand spaces
• A Language of Patterns for Subterm Selection
• On Correctness of Mathematical Texts from a Logical and Practical Point of View
• A learning-based fact selector for Isabelle/HOL
• Flexary connectives in Mizar
• Sledgehammer: judgement day

This page was built for software: Isar