A tableau-like proof procedure for normal modal logics (Q1329745): Difference between revisions

From MaRDI portal
Import240304020342 (talk | contribs)
Set profile property.
ReferenceBot (talk | contribs)
Changed an Item
 
Property / cites work
 
Property / cites work: Q3682464 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q3030268 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Modal Theorem Proving: An Equational Viewpoint / rank
 
Normal rank
Property / cites work
 
Property / cites work: Strategies for modal resolution: Results and problems / rank
 
Normal rank
Property / cites work
 
Property / cites work: TABLEAUX: A general theorem prover for modal logics / rank
 
Normal rank
Property / cites work
 
Property / cites work: Modal resolution in clausal form / rank
 
Normal rank
Property / cites work
 
Property / cites work: Proof methods for modal and intuitionistic logics / rank
 
Normal rank
Property / cites work
 
Property / cites work: First-order modal tableaux / rank
 
Normal rank
Property / cites work
 
Property / cites work: Destructive Modal Resolution / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q4698331 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q3026978 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q4729755 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q3030269 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Semantical Analysis of Modal Logic I Normal Modal Propositional Calculi / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q5339289 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q3718146 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q3768868 / rank
 
Normal rank
Property / cites work
 
Property / cites work: The programming system PRIZ / rank
 
Normal rank
Property / cites work
 
Property / cites work: Semantics-Based Translation Methods for Modal Logics / rank
 
Normal rank
Property / cites work
 
Property / cites work: A Machine-Oriented Logic Based on the Resolution Principle / rank
 
Normal rank
Property / cites work
 
Property / cites work: A study of Kripke-type models for some modal logics by Gentzen's sequential method / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q5560258 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q3999539 / rank
 
Normal rank

Latest revision as of 16:08, 22 May 2024

scientific article
Language Label Description Also known as
English
A tableau-like proof procedure for normal modal logics
scientific article

    Statements

    A tableau-like proof procedure for normal modal logics (English)
    0 references
    0 references
    29 January 1995
    0 references
    This is an extension to modal logic of the following proof search procedure for classical propositional logic: Expand the goal formula \(G\) into conjunctive normal form and apply the resolution method to the resulting set of clauses. Since these rules of expansion are dual to the standard Gentzen-type rules, the author uses the term ``dual clauses''. The Kripke-style formulation used here derives objects \((k_ 1 F_ 1,\dots, k_ n F_ n)\) with the interpretation: Formula \(F_ 1\) is true in the world \(k_ 1,\dots, F_ n\) is true in \(k_ n\). A modal rule for \(\square A\) is the same as a Kripke rule, but the rule for \(\diamondsuit\) is dual to a Kripke rule: Instantiation \(k'A\) of a formula \(k\diamondsuit A\) for a world \(k'\) accessible from \(k\), generates a new branch of the proof search tree. Another source of branching is the rule for \(V\), while the rule for \((A \& B)\) adds both components \(A\), \(B\) to the same branch. Each branch \(\mathcal B\) (at each stage of construction) of the proof search tree generates a clause \(C_{\mathcal B}\) consisting of (possibly negated) new propositional variables \(p_ k\) obtained from formulas \(kp\), \(k\neg p\) present in \(\mathcal B\). The tree is a proof if the set of clauses corresponding to all branches is inconsistent. The latter property can be checked by propositional resolution. Extensions to predicate logics with constant and expanding domains are sketched. Implementation of the method is mentioned, but no test results are presented. It would be interesting to compare this construction with Beth models and to describe a modification for intuitionistic logic which does not require Gödel-Tarski translation.
    0 references
    dual clauses
    0 references
    proof search procedure
    0 references
    proof search tree
    0 references
    0 references
    0 references
    0 references

    Identifiers