Linear resolution for consequence finding

DOI10.1016/0004-3702(92)90030-2zbMath0805.68105OpenAlexW1965184317MaRDI QIDQ1199916

Katsumi Inoue

Publication date: 17 January 1993

Published in: Artificial Intelligence (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0004-3702(92)90030-2

zbMATH Keywords

resolutionconsequence-findingmodel eliminationproduction fieldSOL-resolution

Mathematics Subject Classification ID

Related Items (25)

Translation of first order formulas into ground formulas via a completion theory ⋮ Hypothesis finding based on upward refinement of residue hypotheses. ⋮ A kind of logical compilation for knowledge bases ⋮ Reconsideration of circumscriptive induction with pointwise circumscription ⋮ Upside-down meta-interpretation of the model elimination theorem-proving procedure for deduction and abduction ⋮ Theory of evidence ? A survey of its mathematical foundations, applications and computational aspects ⋮ Completing causal networks by meta-level abduction ⋮ A generic ATMS ⋮ Temporal abductive reasoning about biochemical reactions ⋮ Embedding circumscriptive theories in general disjunctive programs ⋮ Brave induction: a logical framework for learning from incomplete information ⋮ Brave Induction ⋮ First order LUB approximations: characterization and algorithms ⋮ Partition-based logical reasoning for first-order and propositional theories ⋮ Logic programming, abduction and probability. A top-down anytime algorithm for estimating prior and posterior probabilities ⋮ How to Produce Information About a Given Entity Using Automated Deduction Methods ⋮ Mode-Directed Inverse Entailment for Full Clausal Theories ⋮ Embedding Logics in the Local Computation Framework ⋮ Abductive Reasoning on Molecular Interaction Maps ⋮ Model-based diagnostics and probabilistic assumption-based reasoning ⋮ Metatheory of actions: beyond consistency ⋮ A query answering algorithm for Lukaszewicz' general open default theory ⋮ An abductive framework for negation in disjunctive logic programming ⋮ Prioritized logic programming and its application to commonsense reasoning ⋮ Hypothesis finding with proof theoretical appropriateness criteria

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Compiling a default reasoning system into Prolog
• An incremental method for generating prime implicants/implicates
• Saturation, nonmonotonic reasoning and the closed-world assumption
• A logical framework for default reasoning
• A Prolog technology theorem prover: Implementation by an extended Prolog compiler
• On the relationship between circumscription and negation as failure
• An algorithm to compute circumscription
• A circumscriptive theorem prover
• Circumscription - a form of non-monotonic reasoning
• Natural language and logic. International scientific symposium, Hamburg, FRG, 9-11 May 1989. Proceedings
• Refutation graphs
• Linear resolution with selection function
• A note on linear resolution strategies in consequence-finding
• A fixpoint semantics for disjunctive logic programs
• A Machine-Oriented Logic Based on the Resolution Principle
• RST Flip-Flop Input Equations
• A Simplified Format for the Model Elimination Theorem-Proving Procedure
• Two Results on Ordering for Resolution with Merging and Linear Format
• The Problem of Simplifying Truth Functions

This page was built for publication: Linear resolution for consequence finding