Strategies for modal resolution: Results and problems (Q920970)

From MaRDI portal
Revision as of 01:36, 5 March 2024 by Import240304020342 (talk | contribs) (Set profile property.)
scientific article
Language Label Description Also known as
English
Strategies for modal resolution: Results and problems
scientific article

    Statements

    Strategies for modal resolution: Results and problems (English)
    0 references
    0 references
    0 references
    0 references
    1990
    0 references
    Automated theorem proving in modal logics, based on resolution, is a challenging problem and has caused some previous erroneous results. The authors suggest the following strategies for propositional modal logic (in fact for the S4 Kripke system): deletion of subsumed clauses, extensions of classical strategies based on a static constraint, negative resolution. A notion of a Horn clause for modal logics is introduced. An implementation of the linear strategy has already been realized. As previous related works we mention that of L. Fariñas and M. Cialdea.
    0 references
    resolution
    0 references
    propositional modal logic
    0 references
    S4
    0 references
    Horn clause for modal logics
    0 references

    Identifiers

    0 references
    0 references
    0 references
    0 references
    0 references