Institutional Repository

Deduction systems based on resolution

Show simple item record Eisinger, N Ohlbach, HJ 2018-05-28T12:50:54Z 2018-05-28T12:50:54Z 1993
dc.identifier.citation Eisinger N & Ohlbach HJ (1993) Deduction systems based on resolution. South African Computer Journal, Number 9, 1993 en
dc.identifier.issn 2313-7835
dc.description.abstract A general theory of deduction systems is presented The theory is illustrated with deduction systems based on the resolution calculus, in particular with clause graphs. This theory distinguishes four constituents of a deduction system: • the logic, which establishes a notion of semantic entailment; • the calculus, whose rules of inference provide the syntactic counterpart of entailment; • the logical state transition system, which determines the representation of formulae or sets of formulae together with their interrelationships, and also may allow additional operations reducing the search space; • the control, which comprises the criteria used to choose the most promising from among all applicable inference steps. Much of the standard material on resolution is presented in this framework. For the last two levels many alternatives are discussed. Appropriately adjusted notions of soundness, completeness, confluence, and Noetherianness are introduced in order to characterize the properties of particular deduction systems. For more complex deduction systems, where logical and topological phenomena interleave, such properties can be far from obvious. en
dc.language.iso en en
dc.publisher South African Computer Society (SAICSIT) en
dc.subject Automated reasoning en
dc.subject Deduction en
dc.subject Resolution principle en
dc.title Deduction systems based on resolution en
dc.type Article en

Files in this item

This item appears in the following Collection(s)

Show simple item record

Search UnisaIR


My Account