Simulation and synthesis of deduction calculi

Renate A. Schmidt

doi:10.1016/j.entcs.2010.04.016

Simulation and synthesis of deduction calculi

Research output: Contribution to journal › Article › peer-review

Abstract

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 language	English
Pages (from-to)	221-229
Number of pages	8
Journal	Electronic Notes in Theoretical Computer Science
Volume	262
DOIs	https://doi.org/10.1016/j.entcs.2010.04.016
Publication status	Published - May 2010

Keywords

Decidability
Deduction calculus synthesis
Non-classical logic
Resolution
Tableaux

Access to Document

10.1016/j.entcs.2010.04.016

Cite this

@article{1deb50f7e9994aae9625e0a6e9f676b2,

title = "Simulation and synthesis of deduction calculi",

abstract = "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. {\textcopyright} 2010 Elsevier B.V. All rights reserved.",

keywords = "Decidability, Deduction calculus synthesis, Non-classical logic, Resolution, Tableaux",

author = "Schmidt, {Renate A.}",

year = "2010",

month = may,

doi = "10.1016/j.entcs.2010.04.016",

language = "English",

volume = "262",

pages = "221--229",

journal = "Electronic Notes in Theoretical Computer Science",

issn = "1571-0661",

publisher = "Elsevier BV",

}

TY - JOUR

T1 - Simulation and synthesis of deduction calculi

AU - Schmidt, Renate A.

PY - 2010/5

Y1 - 2010/5

N2 - 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.

AB - 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.

KW - Decidability

KW - Deduction calculus synthesis

KW - Non-classical logic

KW - Resolution

KW - Tableaux

U2 - 10.1016/j.entcs.2010.04.016

DO - 10.1016/j.entcs.2010.04.016

M3 - Article

SN - 1571-0661

VL - 262

SP - 221

EP - 229

JO - Electronic Notes in Theoretical Computer Science

JF - Electronic Notes in Theoretical Computer Science

ER -

Simulation and synthesis of deduction calculi

Abstract

Keywords

Access to Document

Fingerprint

Cite this