Resolution-Like Theorem Proving for High-Level Conditions

The tautology problem is the problem to prove the validity of statements. In this paper, we present a calculus for this undecidable problem on graphical conditions, prove its soundness, investigate the necessity of each deduction rule, and discuss practical aspects concerning an implementation. As we use the framework of weak adhesive HLR categories, the calculus is applicable to a number of replacement capable structures, such as Petri-Nets, graphs or hypergraphs. Key words: first-order tautology problem, high-level conditions, theorem proving, resolution, weak adhesive HLR categories

• Type: Conference
• Year: 2008
• Where: GG
• Authors: Karl-Heinz Pennemann
• Keywords: Adhesive Hlr Categories, GG 2008, Tautology Problem, Theoretical Computer Science, Weak Adhesive Hlr