Using resolution for testing modal satisfiability and building models (Q2751044)
From MaRDI portal
 | This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use this page instead for the normal view: Using resolution for testing modal satisfiability and building models |
scientific article; zbMATH DE number 1664327
| Language | Label | Description | Also known as |
|---|---|---|---|
| English | Using resolution for testing modal satisfiability and building models |
scientific article; zbMATH DE number 1664327 |
Statements
21 November 2001
0 references
automated theorem proving
0 references
satisfiability testing
0 references
proof complexity
0 references
translation-based resolution decision procedure
0 references
multi-modal logic
0 references
selection refinement
0 references
Using resolution for testing modal satisfiability and building models (English)
0 references
In this paper a translation-based resolution decision procedure for a multi-modal logic, defined over families of relations, is presented. The relations may satisfy certain frame properties. Different from previous such resolution decision procedures which are based on ordering refinements, this procedure is based on a selection refinement. The procedure has the advantage that it can be used both as a satisfiablity checker and a model builder. It is shown that tableaux and sequent-style proof systems can be polynomially simulated with this procedure.NEWLINENEWLINEFor the entire collection see [Zbl 0963.00028].
0 references
