Correspondences between classical, intuitionistic and uniform provability

DOI10.1016/S0304-3975(99)00177-2zbMath0951.03048OpenAlexW1818789084WikidataQ127857929 ScholiaQ127857929MaRDI QIDQ1575924

Gopalan Nadathur

Publication date: 23 August 2000

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/s0304-3975(99)00177-2

zbMATH Keywords

proof searchintuitionistic provabilityclassical provabilityabstract logic programming languagesderivability relations over sequentsgoal-directednessuniform provability

Mathematics Subject Classification ID

Logic programming (68N17) Proof theory in general (including proof-theoretic semantics) (03F03)

Related Items

Glivenko sequent classes in the light of structural proof theory ⋮ A Survey of the Proof-Theoretic Foundations of Logic Programming ⋮ Glivenko sequent classes and constructive cut elimination in geometric logics

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Orderings for term-rewriting systems
• A proof procedure for the logic of hereditary Harrop formulas
• On Glinvenko sequent classes
• Uniform proofs as a foundation for logic programming
• N-Prolog: An extension of prolog with hypothetical implication. II. Logical foundations, and negation as failure
• A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification
• Contraction-free sequent calculi for intuitionistic logic
• Computation with run time skolemisation (N-Prolog part 3)
• A Proof-theoretic Analysis of Goal-directed Provability
• Uniform provability in classical logic
• Proof-terms for classical and intuitionistic resolution