Simulation and synthesis of deduction calculi

    Research output: Contribution to journalArticlepeer-review


    This paper gives an overview of two methods for automatically or semi-automatically generating deduction calculi from the semantic specification of a logic. One approach is based on simulating deduction approaches with techniques of automated reasoning and first-order resolution. The second approach synthesises sound, complete and terminating tableau calculi directly from the semantic specification of a logic. © 2010 Elsevier B.V. All rights reserved.
    Original languageEnglish
    Pages (from-to)221-229
    Number of pages8
    JournalElectronic Notes in Theoretical Computer Science
    Publication statusPublished - May 2010


    • Decidability
    • Deduction calculus synthesis
    • Non-classical logic
    • Resolution
    • Tableaux


    Dive into the research topics of 'Simulation and synthesis of deduction calculi'. Together they form a unique fingerprint.

    Cite this