Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
421886 | Electronic Notes in Theoretical Computer Science | 2010 | 9 Pages |
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.
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics