Combining Hilbert style and semantic reasoning in a resolution framework

DOI10.1007/BFB0054261MaRDI QIDQ4249899zbMATH OpenFDO

Authors Hans Jürgen Ohlbach

Publication date 17 June 1999

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/BFB0054261

zbMATH Keywords

automated reasoningnonclassical logicsresolutionsemantics of connectives and operators

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Logic in artificial intelligence (68T27)

Review text

A new approach to automated reasoning in nonclassical logics is presented. This approach means that Hilbert-style axioms are translated into first-order logic (FOL) formulae using the semantics of non-classical operators and connectives. The semantics of connectives and operators is turned into FOL equivalences which can be used as rewrite rules. Reasoning is done in a theory resolution framework. There are many opportunities for improving the approach by using a lot of more strategies and heuristics. Some of the strategies can be viewed as decision procedures for some nonclassical logics. Errata list: p. 209, line 8, read \(\forall m\) instead of \(\forall\omega\); p. 210, line 10, read \(\forall m\) instead of \(\exists m\). For the entire collection see [Zbl 0892.00047].

Recommendations

• Automated theorem proving by resolution in non-classical logics
• scientific article; zbMATH DE number 2042611
• scientific article; zbMATH DE number 683345
• Translation Methods for Non-Classical Logics: An Overview

Cited in

(3)

• Calendar Logic
• scientific article; zbMATH DE number 1943847 (Why is no real title available?)
• First-order resolution methods for modal logics

This page was built for publication: Combining Hilbert style and semantic reasoning in a resolution framework

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4249899)