A new methodology for developing deduction methods
From MaRDI portal
Publication:1037405
DOI10.1007/s10472-009-9155-4zbMath1192.68632OpenAlexW2071254558MaRDI QIDQ1037405
Publication date: 16 November 2009
Published in: Annals of Mathematics and Artificial Intelligence (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10472-009-9155-4
Modal logic (including the logic of norms) (03B45) Logic in artificial intelligence (68T27) Logic in computer science (03B70) Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35) Proof theory in general (including proof-theoretic semantics) (03F03)
Related Items
Simulation and Synthesis of Deduction Calculi ⋮ Resolution with order and selection for hybrid logics ⋮ Using tableau to decide description logics with full role negation and identity ⋮ First-Order Resolution Methods for Modal Logics ⋮ Blocking and other enhancements for bottom-up model generation methods
Uses Software
Cites Work
- Peirce algebras
- Hyperresolution for guarded formulae
- Rasiowa-Sikorski deduction systems in computer science applications.
- Single step tableaux for modal logics. Computational properties, complexity and methodology
- Resolution in Modal, Description and Hybrid Logic
- Computational Space Efficiency and Minimal Model Generation for Guarded Formulae
- Splitting through New Proposition Symbols
- A General Tableau Method for Deciding Description Logics, Modal Logics and Related First-Order Fragments
- System Description: Spass Version 3.0
- Blocking and Other Enhancements for Bottom-Up Model Generation Methods
- The relative efficiency of propositional proof systems
- An empirical analysis of modal theorem provers
- Resolution-based methods for modal logics
- A general framework for pattern-driven modal tableaux
- First-Order Resolution Methods for Modal Logics
- Destructive Modal Resolution
- EXPTIME Tableaux with Global Caching for Description Logics with Transitive Roles, Inverse Roles and Role Hierarchies
- A Machine-Oriented Logic Based on the Resolution Principle
- Automated Deduction – CADE-19
- Theory and Applications of Relational Structures as Knowledge Instruments
- An overview of tableau algorithms for description logics
- 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
