Computer Science – Logic in Computer Science
Scientific paper
2010-03-25
EPTCS 21, 2010, pp. 91-98
Computer Science
Logic in Computer Science
Scientific paper
10.4204/EPTCS.21.8
A number of flexible tactic-based logical frameworks are nowadays available that can implement a wide range of mathematical theories using a common higher-order metalanguage. Used as proof assistants, one of the advantages of such powerful systems resides in their responsiveness to extensibility of their reasoning capabilities, being designed over rule-based programming languages that allow the user to build her own `programs to construct proofs' - the so-called proof tactics. The present contribution discusses the implementation of an algorithm that generates sound and complete tableau systems for a very inclusive class of sufficiently expressive finite-valued propositional logics, and then illustrates some of the challenges and difficulties related to the algorithmic formation of automated theorem proving tactics for such logics. The procedure on whose implementation we will report is based on a generalized notion of analyticity of proof systems that is intended to guarantee termination of the corresponding automated tactics on what concerns theoremhood in our targeted logics.
No associations
LandOfFree
Automatic Generation of Proof Tactics for Finite-Valued Logics does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with Automatic Generation of Proof Tactics for Finite-Valued Logics, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Automatic Generation of Proof Tactics for Finite-Valued Logics will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-555892