Isabelle. A generic theorem prover
From MaRDI portal
Publication:1331625
DOI10.1007/BFb0030541zbMath0825.68059MaRDI QIDQ1331625
Publication date: 22 August 1994
Published in: Lecture Notes in Computer Science (Search for Journal in Brave)
Related Items
1998 European Summer Meeting of the Association for Symbolic Logic ⋮ A Proof Theoretic Interpretation of Model Theoretic Hiding ⋮ Towards Logical Frameworks in the Heterogeneous Tool Set Hets ⋮ A UTP approach for rTiMo ⋮ Semi-intelligible Isar proofs from machine-generated proofs ⋮ Integrating Owicki-Gries for C11-style memory models into Isabelle/HOL ⋮ Balancing the load. Leveraging a semantics stack for systems verification ⋮ The undecidability of proof search when equality is a logical connective ⋮ Nominal logic, a first order theory of names and binding ⋮ Formal Logic Definitions for Interchange Languages ⋮ Decidability of Univariate Real Algebra with Predicates for Rational and Integer Powers ⋮ Extracting a DPLL Algorithm ⋮ Symbolic automatic relations and their applications to SMT and CHC solving ⋮ Ordinal arithmetic: Algorithms and mechanization ⋮ Translating a Dependently-Typed Logic to First-Order Logic ⋮ TPS: A hybrid automatic-interactive system for developing proofs ⋮ A proof-centric approach to mathematical assistants ⋮ Computer supported mathematics with \(\Omega\)MEGA ⋮ Structuring metatheory on inductive definitions ⋮ Rewriting conversions implemented with continuations ⋮ Toward compositional verification of interruptible OS kernels and device drivers ⋮ Morphism axioms ⋮ Higher-order rewrite systems and their confluence ⋮ Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols ⋮ A scalable module system ⋮ Towards the Mathematics Software Bus ⋮ A first order logic of effects ⋮ Twenty years of rewriting logic ⋮ A survey on temporal logics for specifying and verifying real-time systems ⋮ A Declarative Language for the Coq Proof Assistant ⋮ A realizability interpretation of Church's simple theory of types ⋮ A complete axiom system for propositional projection temporal logic with cylinder computation model ⋮ Verifying a scheduling protocol of safety-critical systems ⋮ Verified lightweight bytecode verification ⋮ Hoare logic for Java in Isabelle/HOL ⋮ Proofs and Reconstructions ⋮ Reasoning about memory layouts ⋮ Reuse of proofs in software verification ⋮ Admissibility of structural rules for contraction-free systems of intuitionistic logic ⋮ Modelling Attacker’s Knowledge for Cascade Cryptographic Protocols ⋮ Representing model theory in a type-theoretical logical framework ⋮ Automating Algebraic Specifications of Non-freely Generated Data Types ⋮ Verifying OpenJDK's sort method for generic collections ⋮ The Isabelle Framework ⋮ LCF-Style Propositional Simplification with BDDs and SAT Solvers ⋮ Lightweight Separation ⋮ Real Number Calculations and Theorem Proving ⋮ Decidability of bounded higher-order unification ⋮ An approach to automatic deductive synthesis of functional programs ⋮ Automating Event-B invariant proofs by rippling and proof patching ⋮ Automated type-based analysis of injective agreement in the presence of compromised principals ⋮ Machine-Checked Proof-Theory for Propositional Modal Logics ⋮ The seven virtues of simple type theory ⋮ The correctness of a higher-order lazy functional language implementation: An exercise in mechanical theorem proving ⋮ Compensation methods to support cooperative applications: A case study in automated verification of schema requirements for an advanced transaction model ⋮ An embedding of Ruby in Isabelle ⋮ Optimizing proof search in model elimination ⋮ Proof search with set variable instantiation in the Calculus of Constructions ⋮ On the mechanization of the proof of Hessenberg's theorem in coherent logic ⋮ The use of embeddings to provide a clean separation of term and annotation for higher order rippling ⋮ Reasoning about conditional probabilities in a higher-order-logic theorem prover ⋮ The dodecahedral conjecture ⋮ The world's shortest correct exact real arithmetic program? ⋮ A process calculus BigrTiMo of mobile systems and its formal semantics ⋮ From LCF to Isabelle/HOL ⋮ A generic and executable formalization of signature-based Gröbner basis algorithms ⋮ Verification of dynamic bisimulation theorems in Coq ⋮ A UTP semantics for communicating processes with shared variables and its formal encoding in PVS ⋮ Efficiently checking propositional refutations in HOL theorem provers ⋮ Implementing type systems for the IDE with Xsemantics ⋮ Implementing geometric algebra products with binary trees ⋮ Automating Soundness Proofs ⋮ A shape graph logic and a shape system ⋮ Limited second-order functionality in a first-order setting ⋮ Formalization of Entropy Measures in HOL ⋮ Composable Discovery Engines for Interactive Theorem Proving ⋮ Isabelle's metalogic: formalization and proof checker ⋮ Exploring the Foundations of Discrete Analytical Geometry in Isabelle/HOL ⋮ Experiences from exporting major proof assistant libraries ⋮ Mechanized metatheory revisited ⋮ Formalization of geometric algebra in HOL Light ⋮ Towards an Awareness-Based Semantics for Security Protocol Analysis ⋮ A Representation of Fω in LF ⋮ The calculus of constructions as a framework for proof search with set variable instantiation ⋮ Proof-search in type-theoretic languages: An introduction ⋮ Data compression for proof replay ⋮ Performance analysis and functional verification of the stop-and-wait protocol in HOL ⋮ Ours Is to Reason Why ⋮ Graphical reasoning in compact closed categories for quantum computation ⋮ Program development schemata as derived rules ⋮ Logic-independent proof search in logical frameworks (short paper) ⋮ CASL: the Common Algebraic Specification Language. ⋮ Structuring metatheory on inductive definitions ⋮ Theorem proving as constraint solving with coherent logic ⋮ Mechanizing Nonstandard Real Analysis ⋮ A formalization and proof checker for Isabelle's metalogic ⋮ A Meta Linear Logical Framework ⋮ Narrowing and Rewriting Logic: from Foundations to Applications ⋮ Evaluating general purpose automated theorem proving systems ⋮ The future of logic: foundation-independence ⋮ Lax Theory Morphisms ⋮ Formalization of Forcing in Isabelle/ZF ⋮ Efficient second-order matching ⋮ More Church-Rosser proofs (in Isabelle/HOL) ⋮ Ergo 6: A Generic Proof Engine that Uses Prolog Proof Technology ⋮ The Relative Consistency of the Axiom of Choice Mechanized Using Isabelle⁄zf ⋮ I/O automata in Isabelle/HOL ⋮ The formal verification of the ctm approach to forcing ⋮ Towards automated deduction in cP systems ⋮ \textsf{LOGIC}: a Coq library for logics ⋮ Unnamed Item ⋮ Unnamed Item ⋮ A fine-grained semantics for arrays and pointers under weak memory models ⋮ A User-friendly Interface for a Lightweight Verification System ⋮ Integrating Systems around the User: Combining Isabelle, Maple, and QEPCAD in the Proverʼs Palette ⋮ Representing Model Theory in a Type-Theoretical Logical Framework ⋮ A higher-order interpretation of deductive tableau ⋮ PVS Embedding of cCSP Semantic Models and Their Relationship ⋮ A Theoretical Framework for the Higher-Order Cooperation of Numeric Constraint Domains ⋮ Verifying safety critical task scheduling systems in PPTL axiom system ⋮ Trustworthy Graph Algorithms (Invited Talk) ⋮ A practical implementation of simple consequence relations using inductive definitions ⋮ Hybrid interactive theorem proving using nuprl and HOL ⋮ Proof tactics for a theory of state machines in a graphical environment ⋮ RALL: Machine-supported proofs for relation algebra ⋮ Nuprl-Light: An implementation framework for higher-order logics ⋮ Flexary Operators for Formalized Mathematics ⋮ Towards Knowledge Management for HOL Light ⋮ High-Level Theories ⋮ Combining Isabelle and QEPCAD-B in the Prover’s Palette ⋮ Generalized Elimination Inferences, Higher-Level Rules, and the Implications-as-Rules Interpretation of the Sequent Calculus ⋮ Accessible Reasoning with Diagrams: From Cognition to Automation
Uses Software
