Simulation and synthesis of deduction calculi

DOI10.1016/J.ENTCS.2010.04.016MaRDI QIDQ3185770zbMATH OpenOpenAlexFDO

Authors Renate A. Schmidt

Publication date 5 August 2016

Published in Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.entcs.2010.04.016

zbMATH Keywords

decidabilitydeduction calculus synthesisnonclassical logicresolutiontableaux

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Semantics in the theory of computing (68Q55)

Recommendations

• Synthesising terminating tableau calculi for relational logics (invited paper)
• Automated synthesis of tableau calculi
• Automated synthesis of tableau calculi
• A new methodology for developing deduction methods
• scientific article; zbMATH DE number 2090150

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 new methodology for developing deduction methods
• A principle for incorporating axioms into the first-order translation of modal formulae.
• A tableau method for checking rule admissibility in S4
• An empirical analysis of modal theorem provers
• Automated synthesis of tableau calculi
• Blocking and Other Enhancements for Bottom-Up Model Generation Methods
• Functional translation and second-order frame properties of modal logics
• scientific article; zbMATH DE number 1612541 (Why is no real title available?)
• scientific article; zbMATH DE number 1809861 (Why is no real title available?)
• scientific article; zbMATH DE number 5295699 (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
• Resolution decision procedures
• Resolution in modal, description and hybrid logic
• Resolution-based methods for modal logics
• Semantics-Based Translation Methods for Modal Logics
• System Description: Spass Version 3.0
• The axiomatic translation principle for modal logic
• The tableaux work bench
• Using resolution for testing modal satisfiability and building models

Cited in

(9)

• Fixpoint semantics and simulation
• A theory for deductive synthesis of algorithms in the computing milieu
• Synthesising terminating tableau calculi for relational logics (invited paper)
• First-order resolution methods for modal logics
• Mathematical Foundations of Computer Science 2003
• Automated synthesis of tableau calculi
• OUP accepted manuscript
• Automated synthesis of tableau calculi
• Simulation of hybrid circuits in constraint logic programming

Describes a project that uses

Uses Software

• SPASS
• VAMPIRE
• MSPASS

This page was built for publication: Simulation and synthesis of deduction calculi

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3185770)