A logical characterization of forward and backward chaining in the inverse method

DOI10.1007/s10817-007-9091-0zbMath1151.03006OpenAlexW1989085426MaRDI QIDQ928660

Kaustuv Chaudhuri, Greg Price, Frank Pfenning

Publication date: 11 June 2008

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

Full work available at URL: https://doi.org/10.1007/s10817-007-9091-0

zbMATH Keywords

SLD resolutionFocusingHyperresolutionIntuitionistic linear logicInverse method

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Proof-theoretic aspects of linear logic and other substructural logics (03F52)

Related Items

From axioms to synthetic inference rules via focusing, Proof checking and logic programming, Disproving Using the Inverse Method by Iterative Refinement of Finite Approximations, Structural Focalization, A Survey of the Proof-Theoretic Foundations of Logic Programming, Unnamed Item, A semantic framework for proof evidence, Unnamed Item, Multi-focused cut elimination, Expressing additives using multiplicatives and subexponentials, Multi-focused proofs with different polarity assignments, The polarized \(\lambda\)-calculus, Proof Checking and Logic Programming, A framework for proof systems, Efficient Intuitionistic Theorem Proving with the Polarized Inverse Method, Focused and Synthetic Nested Sequents, Subformula linking for intuitionistic logic with application to type theory, Focusing and polarization in linear, intuitionistic, and classical logics

Uses Software

• linTAP
• llprover
• Lolli

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Decision problems for propositional linear logic
• Logic programming in a fragment of intuitionistic linear logic
• The Alexander Method - a technique for the processing of recursive axioms in deductive databases
• Focussing and proof construction
• Linear resolution with selection function
• Locus Solum: From the rules of logic to the logic of rules
• Focusing and Polarization in Intuitionistic Logic
• A Logical Characterization of Forward and Backward Chaining in the Inverse Method
• Logic Programming with Focusing Proofs in Linear Logic
• A new deconstructive logic: linear logic
• Model checking linear logic specifications
• An Intuitionistic Predicate Logic Theorem Prover
• Computer Science Logic
• Automated Deduction – CADE-20
• Types for Proofs and Programs
• The deevolution of concurrent logic programming languages
• FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science