The undecidability of proof search when equality is a logical connective

DOI10.1007/s10472-021-09764-0OpenAlexW3179871171MaRDI QIDQ2134939

Yanyan Li

Publication date: 4 May 2022

Published in: Annals of Mathematics and Artificial Intelligence (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10472-021-09764-0

zbMATH Keywords

undecidabilitysequent calculusunificationequality

Mathematics Subject Classification ID

Proof theory in general (including proof-theoretic semantics) (03F03)

Uses Software

• Isabelle
• Bedwyr
• Abella

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Linear logic
• Nominal abstraction
• The number of proof lines and the size of proofs in first order logic
• The undecidability of the second-order unification problem
• Unification under a mixed prefix
• A unification algorithm for typed \(\bar\lambda\)-calculus
• A proof procedure for the logic of hereditary Harrop formulas
• Isabelle. A generic theorem prover
• The Kreisel length-of-proof problem
• Cut-elimination for a logic with definitions and induction
• Simultaneous rigid E-unification and other decision problems related to the Herbrand theorem
• A proof theory for model checking
• Programming with Higher-Order Logic
• A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification
• Abella: A System for Reasoning about Relational Specifications
• Higher-order pattern complement and the strict λ-calculus
• A proof theory for generic judgments
• New Computational Paradigms
• Least and Greatest Fixed Points in Linear Logic

This page was built for publication: The undecidability of proof search when equality is a logical connective