Simulation and Synthesis of Deduction Calculi

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.

• Type: Journal
• Year: 2010
• Where: ENTCS
• Authors: Renate A. Schmidt
• Keywords: Deduction Calculi, ENTCS 2010, First-order Resolution, Semantic Specification