First-Order Resolution Methods for Modal Logics
From MaRDI portal
Publication:4916086
DOI10.1007/978-3-642-37651-1_15zbMath1383.03031OpenAlexW2113066314MaRDI QIDQ4916086
Renate A. Schmidt, Ullrich Hustadt
Publication date: 19 April 2013
Published in: Programming Logics (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-642-37651-1_15
Modal logic (including the logic of norms) (03B45) Mechanization of proofs and logical operations (03B35)
Related Items (9)
Semantically-guided goal-sensitive reasoning: decision procedures and the Koala prover ⋮ 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} \) ⋮ Deontic Logic for Human Reasoning ⋮ Efficient local reductions to basic modal logic ⋮ A new methodology for developing deduction methods ⋮ Modal Satisfiability via SMT Solving ⋮ Local is best: efficient reductions to modal logic \textsf{K} ⋮ Local reductions for the modal cube
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Deciding expressive description logics in the framework of resolution
- A resolution-based decision procedure for \({\mathcal{SHOIQ}}\).
- Tractable query answering and rewriting under description logic constraints
- A new methodology for developing deduction methods
- The modal logic of `all and only'
- Inaccessible worlds
- Modal languages and bounded fragments of predicate logic
- Decidability by resolution for propositional modal logics
- Tools and techniques in modal logic
- Generalized quantifiers and modal logic
- Refutational theorem proving for hierarchic first-order theories
- Peirce algebras
- Computing circumscription revisited: A reduction algorithm
- Hyperresolution for guarded formulae
- Positive unit hyperresolution tableaux and their application to minimal model generation
- On modal logics characterized by models with relative accessibility relations. II
- Using resolution for testing modal satisfiability and building models
- Decidability of fluted logic with identity
- Single step tableaux for modal logics. Computational properties, complexity and methodology
- Mechanising first-order temporal resolution
- The inverse method for establishing deducibility for logical calculi
- Splitting and reduction heuristics in automatic theorem proving
- Deciding regular grammar logics with converse through first-order logic
- Computational Space Efficiency and Minimal Model Generation for Guarded Formulae
- Splitting through New Proposition Symbols
- Simulation and Synthesis of Deduction Calculi
- Improved Second-Order Quantifier Elimination in Modal Logic
- Implementing a fair monodic temporal logic prover
- CTL-RP: A computation tree logic resolution prover
- System Description: Spass Version 3.0
- Blocking and Other Enhancements for Bottom-Up Model Generation Methods
- Hypertableau Reasoning for Description Logics
- Semantics-Based Translation Methods for Modal Logics
- Modal Theorem Proving: An Equational Viewpoint
- On the Correspondence Between Modal and Classical Logic: an Automated Approach
- Translation Methods for Non-Classical Logics: An Overview
- Undecidable Varieties of Semilattice—ordered Semigroups, of Boolean Algebras with Operators, and logics extending Lambek Calculus
- Rewrite-based Equational Theorem Proving with Selection and Simplification
- Functional translation and second-order frame properties of modal logics
- An empirical analysis of modal theorem provers
- Resolution-based methods for modal logics
- Quine's ‘limits of decision’
- On the Restraining Power of Guards
- A Refined Resolution Calculus for CTL
- Fair Derivations in Monodic Temporal Reasoning
- Optimized Query Rewriting for OWL 2 QL
- Monodic temporal resolution
- The axiomatic translation principle for modal logic
- A Machine-Oriented Logic Based on the Resolution Principle
- Relational and Kleene-Algebraic Methods in Computer Science
- Relational and Kleene-Algebraic Methods in Computer Science
- Clausal temporal resolution
- Automated Deduction – CADE-19
- Automated Deduction – CADE-19
- Theory and Applications of Relational Structures as Knowledge Instruments
This page was built for publication: First-Order Resolution Methods for Modal Logics
