A logical characterization of forward and backward chaining in the inverse method
type: Item
instance of: scholarly article
title: A logical characterization of forward and backward chaining in the inverse method
zbMATH Open document ID: 1151.03006
author: Kaustuv Chaudhuri
author: Frank Pfenning
author: Greg Price
published in: Journal of Automated Reasoning
publication date: 2008-06-11T00:00:00Z
review text: The authors present the focusing system for linear logic. The key feature of focusing is that each logical connective carries an intrinsic attribute, called polarity, that determines its behavior. Polarities may be chosen freely also for atomic propositions as long as duality is consistently maintained. The authors show that proof search on Horn propositions with the inverse method behaves either like hyperresolution or SLD resolution, depending on the chosen polarity for atoms. The focused inverse method therefore directly generalizes these two proof search strategies. Experimental results and an evaluation of the practical benefits of the method for a number of examples from different problem domains are presented.
Mathematics Subject Classification ID: 03B35
Mathematics Subject Classification ID: 03F52
Mathematics Subject Classification ID: 68T15
zbMATH DE Number: 5287718
zbMATH Keywords: Inverse method
zbMATH Keywords: Focusing
zbMATH Keywords: SLD resolution
zbMATH Keywords: Hyperresolution
zbMATH Keywords: Intuitionistic linear logic
reviewed by: Nail Zamov
describes a project that uses: llprover
describes a project that uses: linTAP
describes a project that uses: Lolli
MaRDI profile type: Publication
full work available at URL: s10817-007-9091-0
OpenAlex ID: W1989085426
cites work: Logic Programming with Focusing Proofs in Linear Logic
cites work: Focussing and proof construction
cites work: Model checking linear logic specifications
cites work: Types for Proofs and Programs
cites work: Automated Deduction – CADE-20
cites work: Computer Science Logic
cites work: A Logical Characterization of Forward and Backward Chaining in the Inverse Method
cites work: Q4842975
cites work: A new deconstructive logic: linear logic
cites work: The inverse method
cites work: Locus solum: From the rules of logic to the logic of rules.
cites work: Logic programming in a fragment of intuitionistic linear logic
cites work: FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science
cites work: Linear resolution with selection function
cites work: Focusing and Polarization in Intuitionistic Logic
cites work: Decision problems for propositional linear logic
cites work: Q4263017
cites work: The deevolution of concurrent logic programming languages
cites work: The Alexander Method - a technique for the processing of recursive axioms in deductive databases
cites work: An Intuitionistic Predicate Logic Theorem Prover
cites work: Q4364504
DOI: 10.1007/S10817-007-9091-0
description: scientific article; zbMATH DE number 5287718