The foundation of a generic theorem prover

DOI10.1007/BF00248324zbMath0679.68173OpenAlexW1995955735WikidataQ57382729 ScholiaQ57382729MaRDI QIDQ1823013

Publication date: 1989

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/bf00248324

zbMATH Keywords

LCF higher-order logic natural deduction logical framework higher-order unification Standard ML ISABELLE meta reasoning

Mathematics Subject Classification ID

Related Items

Generating custom set theories with non-set structured objects ⋮ Inductive families ⋮ Formal verification of C systems code. Structured types, separation logic and theorem proving ⋮ Formalization of Forcing in Isabelle/ZF ⋮ Fresh logic: Proof-theory and semantics for FM and nominal techniques ⋮ An overview of LP, the Larch Prover ⋮ Rewriting, and equational unification: the higher-order cases ⋮ Higher-order superposition for dependent types ⋮ Computational logic: its origins and applications ⋮ TPS: A hybrid automatic-interactive system for developing proofs ⋮ Ergo 6: A Generic Proof Engine that Uses Prolog Proof Technology ⋮ The Relative Consistency of the Axiom of Choice Mechanized Using Isabelle⁄zf ⋮ Formalising mathematics -- in praxis; a mathematician's first experiences with Isabelle/HOL and the why and how of getting started ⋮ Program tactics and logic tactics ⋮ TPS: A theorem-proving system for classical type theory ⋮ Irrationality and Transcendence Criteria for Infinite Series in Isabelle/HOL ⋮ Proving and rewriting ⋮ A metatheory of a mechanized object theory ⋮ A Survey of the Proof-Theoretic Foundations of Logic Programming ⋮ A formalised theorem in the partition calculus ⋮ Semantics for abstract clauses ⋮ Rensets and renaming-based recursion for syntax with bindings extended version ⋮ The formal verification of the ctm approach to forcing ⋮ Wetzel: formalisation of an undecidable problem linked to the continuum hypothesis ⋮ Equivalences between logics and their representing type theories ⋮ A semantic framework for proof evidence ⋮ Automation for interactive proof: first prototype ⋮ A functional programming approach to the specification and verification of concurrent systems ⋮ Term rewriting and beyond -- theorem proving in Isabelle ⋮ Unnamed Item ⋮ A mechanized proof of the basic perturbation lemma ⋮ Unnamed Item ⋮ Forum: A multiple-conclusion specification logic ⋮ A formalized general theory of syntax with bindings: extended version ⋮ Program development in constructive type theory ⋮ R n - and G n -logics ⋮ Using typed lambda calculus to implement formal systems on a machine ⋮ Unification under a mixed prefix ⋮ Theo: An interactive proof development system ⋮ Curry-Howard for incomplete first-order logic derivations using one-and-a-half level terms ⋮ Partiality and recursion in interactive theorem provers – an overview ⋮ A framework for proof systems ⋮ The control layer in open mechanized reasoning systems: Annotations and tactics ⋮ From LCF to Isabelle/HOL ⋮ Formalization of the Poincaré disc model of hyperbolic geometry ⋮ On the Mints Hierarchy in First-Order Intuitionistic Logic ⋮ Mollusc a general proof-development shell for sequent-based logics ⋮ Isabelle's metalogic: formalization and proof checker ⋮ A practical implementation of simple consequence relations using inductive definitions ⋮ Unnamed Item ⋮ Encoding Generic Judgments ⋮ Proof-search in type-theoretic languages: An introduction ⋮ Program development schemata as derived rules ⋮ REWRITING WITH STRATEGIES IN $\mathsf{ELAN}$: A FUNCTIONAL SEMANTICS ⋮ Logic-Free Reasoning in Isabelle/Isar ⋮ Term-generic logic ⋮ Implementing tactics and tacticals in a higher-order logic programming language ⋮ Experimenting with Isabelle in ZF set theory ⋮ Rensets and renaming-based recursion for syntax with bindings ⋮ A Shell for Generic Interactive Proof Search ⋮ A formalization and proof checker for Isabelle's metalogic ⋮ Set theory for verification. I: From foundations to functions ⋮ The practice of logical frameworks

Uses Software

Cites Work