A new methodology for developing deduction methods
From MaRDI portal
Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35) Modal logic (including the logic of norms) (03B45) Logic in computer science (03B70) Proof theory in general (including proof-theoretic semantics) (03F03) Logic in artificial intelligence (68T27)
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
Cites work
- A general framework for pattern-driven modal tableaux
- A General Tableau Method for Deciding Description Logics, Modal Logics and Related First-Order Fragments
- A Machine-Oriented Logic Based on the Resolution Principle
- A principle for incorporating axioms into the first-order translation of modal formulae.
- An empirical analysis of modal theorem provers
- An overview of tableau algorithms for description logics
- Blocking and Other Enhancements for Bottom-Up Model Generation Methods
- Computational Space Efficiency and Minimal Model Generation for Guarded Formulae
- Destructive Modal Resolution
- Encoding two-valued nonclassical logics in classical logic
- EXPTIME Tableaux with Global Caching for Description Logics with Transitive Roles, Inverse Roles and Role Hierarchies
- First-order resolution methods for modal logics
- scientific article; zbMATH DE number 1612541 (Why is no real title available?)
- scientific article; zbMATH DE number 1614714 (Why is no real title available?)
- scientific article; zbMATH DE number 1809861 (Why is no real title available?)
- scientific article; zbMATH DE number 1809862 (Why is no real title available?)
- scientific article; zbMATH DE number 5295699 (Why is no real title available?)
- scientific article; zbMATH DE number 48763 (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 1507191 (Why is no real title available?)
- scientific article; zbMATH DE number 2090304 (Why is no real title available?)
- scientific article; zbMATH DE number 3198011 (Why is no real title available?)
- Hyperresolution for guarded formulae
- Paramodulation-based theorem proving
- Peirce algebras
- Rasiowa-Sikorski deduction systems in computer science applications.
- Resolution decision procedures
- Resolution in modal, description and hybrid logic
- Resolution theorem proving
- Resolution-based methods for modal logics
- Second-order quantifier elimination. Foundations, computational aspects and applications
- Single step tableaux for modal logics. Computational properties, complexity and methodology
- Splitting through new proposition symbols
- System Description: Spass Version 3.0
- Tableau methods for modal and temporal logics
- The relative efficiency of propositional proof systems
- Theory and Applications of Relational Structures as Knowledge Instruments
- Using resolution for testing modal satisfiability and building models
Cited in
(8)- Blocking and other enhancements for bottom-up model generation methods
- Resolution with order and selection for hybrid logics
- Resolution in modal, description and hybrid logic
- Simulation and synthesis of deduction calculi
- A new approach to derivation
- First-order resolution methods for modal logics
- Using tableau to decide description logics with full role negation and identity
- Theory exploration powered by deductive synthesis
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)
