A new methodology for developing deduction methods
DOI10.1007/S10472-009-9155-4zbMATH Open1192.68632OpenAlexW2071254558MaRDI QIDQ1037405FDOQ1037405
Authors: Renate A. Schmidt 
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
Recommendations
- scientific article; zbMATH DE number 1552513
- A new deductive approach to planning
- A new probabilistic induction method
- A new approach to derivation
- A vision for automated deduction rooted in the connection method
- scientific article; zbMATH DE number 1552519
- A methodology for using a default and abductive reasoning system
- scientific article; zbMATH DE number 785048
- An inductive method for inexact reasoning
- scientific article; zbMATH DE number 3972241
Modal logic (including the logic of norms) (03B45) Proof theory in general (including proof-theoretic semantics) (03F03) Logic in artificial intelligence (68T27) Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35) Logic in computer science (03B70)
Cites Work
- Title not available (Why is that?)
- Title not available (Why is that?)
- Resolution theorem proving
- Title not available (Why is that?)
- A Machine-Oriented Logic Based on the Resolution Principle
- Title not available (Why is that?)
- Resolution decision procedures
- The relative efficiency of propositional proof systems
- A General Tableau Method for Deciding Description Logics, Modal Logics and Related First-Order Fragments
- Blocking and Other Enhancements for Bottom-Up Model Generation Methods
- Tableau methods for modal and temporal logics
- Paramodulation-based theorem proving
- Splitting through new proposition symbols
- Title not available (Why is that?)
- An empirical analysis of modal theorem provers
- EXPTIME Tableaux with Global Caching for Description Logics with Transitive Roles, Inverse Roles and Role Hierarchies
- An overview of tableau algorithms for description logics
- Rasiowa-Sikorski deduction systems in computer science applications.
- Single step tableaux for modal logics. Computational properties, complexity and methodology
- Second-order quantifier elimination. Foundations, computational aspects and applications
- System Description: Spass Version 3.0
- Encoding two-valued nonclassical logics in classical logic
- Resolution-based methods for modal logics
- Title not available (Why is that?)
- Destructive Modal Resolution
- Resolution in modal, description and hybrid logic
- A principle for incorporating axioms into the first-order translation of modal formulae.
- Hyperresolution for guarded formulae
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Peirce algebras
- Using resolution for testing modal satisfiability and building models
- Computational Space Efficiency and Minimal Model Generation for Guarded Formulae
- Title not available (Why is that?)
- A general framework for pattern-driven modal tableaux
- First-order resolution methods for modal logics
- Theory and Applications of Relational Structures as Knowledge Instruments
Cited In (8)
- Blocking and other enhancements for bottom-up model generation methods
- Simulation and synthesis of deduction calculi
- A new approach to derivation
- Using tableau to decide description logics with full role negation and identity
- Resolution with order and selection for hybrid logics
- Resolution in modal, description and hybrid logic
- Theory exploration powered by deductive synthesis
- First-order resolution methods for modal logics
Uses Software
This page was built for publication: A new methodology for developing deduction methods
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1037405)
