Resolution-Like Theorem Proving for High-Level Conditions

DOI10.1007/978-3-540-87405-8_20zbMath1175.03008OpenAlexW1810787746MaRDI QIDQ3540406

Karl-Heinz Pennemann

Publication date: 20 November 2008

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-540-87405-8_20

zbMATH Keywords

theorem provingresolutionfirst-order tautology problemhigh-level conditionsweak adhesive HLR categories

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Grammars and rewriting systems (68Q42)

Related Items

Theorem proving graph grammars with attributes and negative application conditions, On the Specification and Verification of Model Transformations, Interactive and automated proofs for graph transformations, Symbolic graphs for attributed graph constraints, Unnamed Item, Unnamed Item, A navigational logic for reasoning about graph properties, Reasoning with graph constraints, Institutions for navigational logics for graphical structures, Rewriting theory for the life sciences: a unifying theory of CTMC semantics

Uses Software

• VAMPIRE

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Graph-based specification of access control policies
• Fundamentals of algebraic graph transformation
• Modeling and Verifying Graph Transformations in Proof Assistants
• Attributed Graph Constraints
• Weakest Preconditions for High-Level Programs
• Correctness of high-level transformation systems relative to nested conditions
• An Algorithm for Approximating the Satisfiability Problem of High-level Conditions
• A Logic of Graph Constraints
• A Machine-Oriented Logic Based on the Resolution Principle
• Formal Methods in Software and Systems Modeling