Automating proof search when equality is a logical connective
From MaRDI portal
Cites work
- A formulation of the simple theory of types.
- A framework for defining logics
- A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification
- A proof procedure for the logic of hereditary Harrop formulas
- A proof theory for generic judgments
- A semantic framework for proof evidence
- A unification algorithm for typed \(\bar\lambda\)-calculus
- Abella: a system for reasoning about relational specifications
- An insider's look at LF type reconstruction: everything you (n)ever wanted to know
- Cut-elimination for a logic with definitions and induction
- Equational problems and disunification
- Functions-as-constructors higher-order unification: extended pattern unification
- scientific article; zbMATH DE number 4053062 (Why is no real title available?)
- scientific article; zbMATH DE number 42059 (Why is no real title available?)
- scientific article; zbMATH DE number 65531 (Why is no real title available?)
- Logical frameworks
- Programming with higher-order logic.
- The Proof Certifier Checkers
- The undecidability of proof search when equality is a logical connective
- Theory and practice of constraint handling rules
- Third order matching is decidable
- Translating between implicit and explicit versions of proof
- Unification under a mixed prefix
- Uniform proofs as a foundation for logic programming
- Untersuchungen über das logische Schließen. I.
This page was built for publication: Automating proof search when equality is a logical connective
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q7411296)
