First-order resolution methods for modal logics
From MaRDI portal
Recommendations
Cites work
- A Machine-Oriented Logic Based on the Resolution Principle
- A new methodology for developing deduction methods
- A principle for incorporating axioms into the first-order translation of modal formulae.
- A Refined Resolution Calculus for CTL
- A resolution-based decision procedure for \({\mathcal{SHOIQ}}\).
- An empirical analysis of modal theorem provers
- Blocking and Other Enhancements for Bottom-Up Model Generation Methods
- Clausal temporal resolution
- Computational Space Efficiency and Minimal Model Generation for Guarded Formulae
- Computing circumscription revisited: A reduction algorithm
- CTL-RP: A computation tree logic resolution prover
- Decidability by resolution for propositional modal logics
- Decidability of fluted logic with identity
- Deciding expressive description logics in the framework of resolution
- Deciding regular grammar logics with converse through first-order logic
- Encoding two-valued nonclassical logics in classical logic
- Fair Derivations in Monodic Temporal Reasoning
- Functional translation and second-order frame properties of modal logics
- Generalized quantifiers and modal logic
- scientific article; zbMATH DE number 1612541 (Why is no real title available?)
- scientific article; zbMATH DE number 1614696 (Why is no real title available?)
- scientific article; zbMATH DE number 1614697 (Why is no real title available?)
- scientific article; zbMATH DE number 1614714 (Why is no real title available?)
- scientific article; zbMATH DE number 1809862 (Why is no real title available?)
- scientific article; zbMATH DE number 4148058 (Why is no real title available?)
- scientific article; zbMATH DE number 4128785 (Why is no real title available?)
- scientific article; zbMATH DE number 1267561 (Why is no real title available?)
- scientific article; zbMATH DE number 1303346 (Why is no real title available?)
- scientific article; zbMATH DE number 1341467 (Why is no real title available?)
- scientific article; zbMATH DE number 1341606 (Why is no real title available?)
- scientific article; zbMATH DE number 1341614 (Why is no real title available?)
- scientific article; zbMATH DE number 517065 (Why is no real title available?)
- scientific article; zbMATH DE number 1735878 (Why is no real title available?)
- scientific article; zbMATH DE number 1028833 (Why is no real title available?)
- scientific article; zbMATH DE number 1950272 (Why is no real title available?)
- scientific article; zbMATH DE number 1507191 (Why is no real title available?)
- scientific article; zbMATH DE number 1552532 (Why is no real title available?)
- scientific article; zbMATH DE number 218546 (Why is no real title available?)
- scientific article; zbMATH DE number 2090304 (Why is no real title available?)
- scientific article; zbMATH DE number 2090305 (Why is no real title available?)
- scientific article; zbMATH DE number 834561 (Why is no real title available?)
- scientific article; zbMATH DE number 1421198 (Why is no real title available?)
- scientific article; zbMATH DE number 3351504 (Why is no real title available?)
- Hyperresolution for guarded formulae
- Hypertableau reasoning for description logics
- Implementing a fair monodic temporal logic prover
- Improved Second-Order Quantifier Elimination in Modal Logic
- Inaccessible worlds
- Mechanising first-order temporal resolution
- Modal languages and bounded fragments of predicate logic
- Modal logic
- Modal Theorem Proving: An Equational Viewpoint
- Monodic temporal resolution
- On modal logics characterized by models with relative accessibility relations. II
- On the Correspondence Between Modal and Classical Logic: an Automated Approach
- On the Restraining Power of Guards
- Optimized query rewriting for OWL 2 QL
- Paramodulation-based theorem proving
- Peirce algebras
- Positive unit hyperresolution tableaux and their application to minimal model generation
- Quine's ‘limits of decision’
- Refutational theorem proving for hierarchic first-order theories
- Relational and Kleene-Algebraic Methods in Computer Science
- Relational and Kleene-Algebraic Methods in Computer Science
- Resolution decision procedures
- Resolution theorem proving
- Resolution-based methods for modal logics
- Rewrite-based Equational Theorem Proving with Selection and Simplification
- Second-order quantifier elimination. Foundations, computational aspects and applications
- Semantics-Based Translation Methods for Modal Logics
- Simulation and synthesis of deduction calculi
- Single step tableaux for modal logics. Computational properties, complexity and methodology
- Splitting and reduction heuristics in automatic theorem proving
- Splitting through new proposition symbols
- System Description: Spass Version 3.0
- Tableau methods for modal and temporal logics
- The axiomatic translation principle for modal logic
- The inverse method for establishing deducibility for logical calculi
- The modal logic of `all and only'
- The model evolution calculus.
- Theory and Applications of Relational Structures as Knowledge Instruments
- Tools and techniques in modal logic
- Tractable query answering and rewriting under description logic constraints
- Translation Methods for Non-Classical Logics: An Overview
- Undecidable Varieties of Semilattice—ordered Semigroups, of Boolean Algebras with Operators, and logics extending Lambek Calculus
- Using resolution for testing modal satisfiability and building models
Cited in
(22)- A new methodology for developing deduction methods
- Resolution for some first-order modal systems
- Efficient local reductions to basic modal logic
- Local is best: efficient reductions to modal logic \textsf{K}
- Local reductions for the modal cube
- Designing normative theories for ethical and legal reasoning: \textsc{LogiKEy} framework, methodology, and tool support
- Pay-as-you-go consequence-based reasoning for the description logic \(\mathcal{SROIQ} \)
- scientific article; zbMATH DE number 1612541 (Why is no real title available?)
- Resolution in modal, description and hybrid logic
- Towards resolution-based reasoning for connected logics
- Formalization of the Resolution Calculus for First-Order Logic
- HOL Based First-Order Modal Logic Provers
- On First-Order Model-Based Reasoning
- scientific article; zbMATH DE number 5295699 (Why is no real title available?)
- scientific article; zbMATH DE number 3932427 (Why is no real title available?)
- scientific article; zbMATH DE number 1341615 (Why is no real title available?)
- Resolution-based calculi for modal and temporal logics
- Deontic logic for human reasoning
- Modal Satisfiability via SMT Solving
- Semantically-guided goal-sensitive reasoning: decision procedures and the Koala prover
- Model construction for modal clauses
- First-order automatic literal model generation
This page was built for publication: First-order resolution methods for modal logics
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4916086)
