First-Order Resolution Methods for Modal Logics (Q4916086): Difference between revisions

@@ Property / describes a project that uses @@
+CTL-RP
@@ Property / describes a project that uses: CTL-RP / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+TRP++
@@ Property / describes a project that uses: TRP++ / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+SPASS
@@ Property / describes a project that uses: SPASS / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+E Theorem Prover
@@ Property / describes a project that uses: E Theorem Prover / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / full work available at URL @@
+https://doi.org/10.1007/978-3-642-37651-1_15
+Normal rank
@@ Property / OpenAlex ID @@
+W2113066314
@@ Property / OpenAlex ID: W2113066314 / rank @@
+Normal rank
@@ Property / cites work @@
+Modal languages and bounded fragments of predicate logic
+Normal rank
@@ Property / cites work @@
+Q4860647
@@ Property / cites work: Q4860647 / rank @@
+Normal rank
@@ Property / cites work @@
+Modal Theorem Proving: An Equational Viewpoint
@@ Property / cites work: Modal Theorem Proving: An Equational Viewpoint / rank @@
+Normal rank
@@ Property / cites work @@
+Rewrite-based Equational Theorem Proving with Selection and Simplification
+Normal rank
@@ Property / cites work @@
+Q4524792
@@ Property / cites work: Q4524792 / rank @@
+Normal rank
@@ Property / cites work @@
+Q2751353
@@ Property / cites work: Q2751353 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4282593
@@ Property / cites work: Q4282593 / rank @@
+Normal rank
@@ Property / cites work @@
+Refutational theorem proving for hierarchic first-order theories
+Normal rank
@@ Property / cites work @@
+Q2723420
@@ Property / cites work: Q2723420 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4263006
@@ Property / cites work: Q4263006 / rank @@
+Normal rank
@@ Property / cites work @@
+Blocking and Other Enhancements for Bottom-Up Model Generation Methods
+Normal rank
@@ Property / cites work @@
+Automated Deduction – CADE-19
@@ Property / cites work: Automated Deduction – CADE-19 / rank @@
+Normal rank
@@ Property / cites work @@
+Q2744124
@@ Property / cites work: Q2744124 / rank @@
+Normal rank
@@ Property / cites work @@
+Splitting and reduction heuristics in automatic theorem proving
+Normal rank
@@ Property / cites work @@
+Peirce algebras
@@ Property / cites work: Peirce algebras / rank @@
+Normal rank
@@ Property / cites work @@
+Positive unit hyperresolution tableaux and their application to minimal model generation
+Normal rank
@@ Property / cites work @@
+Q4235432
@@ Property / cites work: Q4235432 / rank @@
+Normal rank
@@ Property / cites work @@
+Optimized Query Rewriting for OWL 2 QL
@@ Property / cites work: Optimized Query Rewriting for OWL 2 QL / rank @@
+Normal rank
@@ Property / cites work @@
+Splitting through New Proposition Symbols
@@ Property / cites work: Splitting through New Proposition Symbols / rank @@
+Normal rank
@@ Property / cites work @@
+Resolution-based methods for modal logics
@@ Property / cites work: Resolution-based methods for modal logics / rank @@
+Normal rank
@@ Property / cites work @@
+Generalized quantifiers and modal logic
@@ Property / cites work: Generalized quantifiers and modal logic / rank @@
+Normal rank
@@ Property / cites work @@
+Monodic temporal resolution
@@ Property / cites work: Monodic temporal resolution / rank @@
+Normal rank
@@ Property / cites work @@
+Deciding regular grammar logics with converse through first-order logic
+Normal rank
@@ Property / cites work @@
+On modal logics characterized by models with relative accessibility relations. II
+Normal rank
@@ Property / cites work @@
+Computing circumscription revisited: A reduction algorithm
+Normal rank
@@ Property / cites work @@
+Q2751377
@@ Property / cites work: Q2751377 / rank @@
+Normal rank
@@ Property / cites work @@
+Clausal temporal resolution
@@ Property / cites work: Clausal temporal resolution / rank @@
+Normal rank
@@ Property / cites work @@
+Q3543581
@@ Property / cites work: Q3543581 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4329239
@@ Property / cites work: Q4329239 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4694250
@@ Property / cites work: Q4694250 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3478385
@@ Property / cites work: Q3478385 / rank @@
+Normal rank
@@ Property / cites work @@
+Computational Space Efficiency and Minimal Model Generation for Guarded Formulae
+Normal rank
@@ Property / cites work @@
+Q4809060
@@ Property / cites work: Q4809060 / rank @@
+Normal rank
@@ Property / cites work @@
+Hyperresolution for guarded formulae
@@ Property / cites work: Hyperresolution for guarded formulae / rank @@
+Normal rank
@@ Property / cites work @@
+Relational and Kleene-Algebraic Methods in Computer Science
+Normal rank
@@ Property / cites work @@
+Q2753601
@@ Property / cites work: Q2753601 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4263155
@@ Property / cites work: Q4263155 / rank @@
+Normal rank
@@ Property / cites work @@
+On the Restraining Power of Guards
@@ Property / cites work: On the Restraining Power of Guards / rank @@
+Normal rank
@@ Property / cites work @@
+Q2723419
@@ Property / cites work: Q2723419 / rank @@
+Normal rank
@@ Property / cites work @@
+Inaccessible worlds
@@ Property / cites work: Inaccessible worlds / rank @@
+Normal rank
@@ Property / cites work @@
+The modal logic of `all and only'
@@ Property / cites work: The modal logic of `all and only' / rank @@
+Normal rank
@@ Property / cites work @@
+Deciding expressive description logics in the framework of resolution
+Normal rank
@@ Property / cites work @@
+An empirical analysis of modal theorem provers
@@ Property / cites work: An empirical analysis of modal theorem provers / rank @@
+Normal rank
@@ Property / cites work @@
+Q4263163
@@ Property / cites work: Q4263163 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4503911
@@ Property / cites work: Q4503911 / rank @@
+Normal rank
@@ Property / cites work @@
+Q2721185
@@ Property / cites work: Q2721185 / rank @@
+Normal rank
@@ Property / cites work @@
+Using resolution for testing modal satisfiability and building models
+Normal rank
@@ Property / cites work @@
+A resolution-based decision procedure for \({\mathcal{SHOIQ}}\).
+Normal rank
@@ Property / cites work @@
+Mechanising first-order temporal resolution
@@ Property / cites work: Mechanising first-order temporal resolution / rank @@
+Normal rank
@@ Property / cites work @@
+Tools and techniques in modal logic
@@ Property / cites work: Tools and techniques in modal logic / rank @@
+Normal rank
@@ Property / cites work @@
+Undecidable Varieties of Semilattice—ordered Semigroups, of Boolean Algebras with Operators, and logics extending Lambek Calculus
+Normal rank
@@ Property / cites work @@
+Fair Derivations in Monodic Temporal Reasoning
@@ Property / cites work: Fair Derivations in Monodic Temporal Reasoning / rank @@
+Normal rank
@@ Property / cites work @@
+Implementing a fair monodic temporal logic prover
@@ Property / cites work: Implementing a fair monodic temporal logic prover / rank @@
+Normal rank
@@ Property / cites work @@
+The inverse method for establishing deducibility for logical calculi
+Normal rank
@@ Property / cites work @@
+Single step tableaux for modal logics. Computational properties, complexity and methodology
+Normal rank
@@ Property / cites work @@
+Hypertableau Reasoning for Description Logics
@@ Property / cites work: Hypertableau Reasoning for Description Logics / rank @@
+Normal rank
@@ Property / cites work @@
+Q2751359
@@ Property / cites work: Q2751359 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4946227
@@ Property / cites work: Q4946227 / rank @@
+Normal rank
@@ Property / cites work @@
+Semantics-Based Translation Methods for Modal Logics
+Normal rank
@@ Property / cites work @@
+Translation Methods for Non-Classical Logics: An Overview
+Normal rank
@@ Property / cites work @@
+Q4249899
@@ Property / cites work: Q4249899 / rank @@
+Normal rank
@@ Property / cites work @@
+Q2751373
@@ Property / cites work: Q2751373 / rank @@
+Normal rank
@@ Property / cites work @@
+Functional translation and second-order frame properties of modal logics
+Normal rank
@@ Property / cites work @@
+Tractable query answering and rewriting under description logic constraints
+Normal rank
@@ Property / cites work @@
+Decidability of fluted logic with identity
@@ Property / cites work: Decidability of fluted logic with identity / rank @@
+Normal rank
@@ Property / cites work @@
+Quine's ‘limits of decision’
@@ Property / cites work: Quine's ‘limits of decision’ / rank @@
+Normal rank
@@ Property / cites work @@
+Q5626600
@@ Property / cites work: Q5626600 / rank @@
+Normal rank
@@ Property / cites work @@
+A Machine-Oriented Logic Based on the Resolution Principle
+Normal rank
@@ Property / cites work @@
+Decidability by resolution for propositional modal logics
+Normal rank
@@ Property / cites work @@
+Improved Second-Order Quantifier Elimination in Modal Logic
+Normal rank
@@ Property / cites work @@
+A new methodology for developing deduction methods
+Normal rank
@@ Property / cites work @@
+Simulation and Synthesis of Deduction Calculi
@@ Property / cites work: Simulation and Synthesis of Deduction Calculi / rank @@
+Normal rank
@@ Property / cites work @@
+Q2723441
@@ Property / cites work: Q2723441 / rank @@
+Normal rank
@@ Property / cites work @@
+Theory and Applications of Relational Structures as Knowledge Instruments
+Normal rank
@@ Property / cites work @@
+Automated Deduction – CADE-19
@@ Property / cites work: Automated Deduction – CADE-19 / rank @@
+Normal rank
@@ Property / cites work @@
+The axiomatic translation principle for modal logic
+Normal rank
@@ Property / cites work @@
+Relational and Kleene-Algebraic Methods in Computer Science
+Normal rank
@@ Property / cites work @@
+Q3150301
@@ Property / cites work: Q3150301 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4412870
@@ Property / cites work: Q4412870 / rank @@
+Normal rank
@@ Property / cites work @@
+On the Correspondence Between Modal and Classical Logic: an Automated Approach
+Normal rank
@@ Property / cites work @@
+Q4342096
@@ Property / cites work: Q4342096 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4809064
@@ Property / cites work: Q4809064 / rank @@
+Normal rank
@@ Property / cites work @@
+System Description: Spass Version 3.0
@@ Property / cites work: System Description: Spass Version 3.0 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4207883
@@ Property / cites work: Q4207883 / rank @@
+Normal rank
@@ Property / cites work @@
+A Refined Resolution Calculus for CTL
@@ Property / cites work: A Refined Resolution Calculus for CTL / rank @@
+Normal rank
@@ Property / cites work @@
+CTL-RP: A computation tree logic resolution prover
+Normal rank