2011/01/01 by Vincent Aravantinos, Aravantinos, Vincent, Nicolas Peltier +2
Computer Science · #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #Semantic Web and Ontologies #cs.AI
paper · pdf · doi:10.48550/arxiv.1106.2692
arxiv created 2011/06/14 · arxiv updated 2015/03/19
Two distinct algorithms are presented to extract (schemata of) resolution proofs from closed tableaux for propositional schemata. The first one handles the most efficient version of the tableau calculus but generates very complex derivations (denoted by rather elaborate rewrite systems). The second one has the advantage that much simpler systems can be obtained, however the considered proof procedure is less efficient.