First-order resolution methods for modal logics
From MaRDI portal
Recommendations
Cites work
- A Machine-Oriented Logic Based on the Resolution Principle
- A new clausal class decidable by hyperresolution
- 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 decision procedure for fluted logic
- 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
- Combining Hilbert style and semantic reasoning in a resolution framework
- Computational Space Efficiency and Minimal Model Generation for Guarded Formulae
- Computing circumscription revisited: A reduction algorithm
- CTL-RP: A computation tree logic resolution prover
- DCTP 1. 2 -- system abstract
- 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
- Decision procedures for guarded logics
- Efficient minimal model generation using branching lemmas
- Encoding two-valued nonclassical logics in classical logic
- Fair Derivations in Monodic Temporal Reasoning
- FDPLL -- a first-order Davis-Putnam-Logeman-Loveland procedure
- Functional translation and second-order frame properties of modal logics
- Generalized quantifiers and modal logic
- 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 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 1552532 (Why is no real title available?)
- scientific article; zbMATH DE number 218546 (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
- Issues of decidability for description logics in the framework of resolution
- Maslov's class K revisited
- Mechanising first-order temporal resolution
- Merge path improvements for minimal model hyper tableaux
- Modal languages and bounded fragments of predicate logic
- Modal logic
- Modal Theorem Proving: An Equational Viewpoint
- Monodic temporal resolution
- MSPASS: Modal reasoning by translation and first-order 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
- Resolution decision procedures
- Resolution theorem proving
- Resolution-based methods for modal logics
- Rewrite-based Equational Theorem Proving with Selection and Simplification
- SCAN is complete for all Sahlqvist formulae
- 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
- SPASS version 2.0
- 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
- Two proof systems for Peirce algebras
- 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
(23)- 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} \)
- MSPASS: Modal reasoning by translation and first-order resolution
- 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?)
- Prefixed resolution. A resolution method for modal and description logics
- 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
- Faithful Logic Embeddings in HOL — Deep and Shallow (Isabelle/HOL dataset)
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)
