Combining Hilbert style and semantic reasoning in a resolution framework (Q4249899)
From MaRDI portal
!
This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use the normal view instead:
scientific article; zbMATH DE number 1303346
| Language | Label | Description | Also known as |
|---|---|---|---|
| default for all languages | No label defined |
||
| English | Combining Hilbert style and semantic reasoning in a resolution framework |
scientific article; zbMATH DE number 1303346 |
Statements
17 June 1999
0 references
automated reasoning
0 references
nonclassical logics
0 references
semantics of connectives and operators
0 references
resolution
0 references
0.7179940342903137
0 references
0.6844319701194763
0 references
Combining Hilbert style and semantic reasoning in a resolution framework (English)
0 references
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].
0 references
