Resolution-Like Theorem Proving for High-Level Conditions

DOI10.1007/978-3-540-87405-8_20MaRDI QIDQ3540406zbMATH OpenOpenAlexFDO

Authors 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

resolutiontheorem provingfirst-order tautology problemhigh-level conditionsweak adhesive HLR categories

Mathematics Subject Classification ID

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

Recommendations

• Comparing approaches to resolution based higher-order theorem proving
• scientific article; zbMATH DE number 2222011
• Theorem-proving with resolution and superposition
• Resolution theorem proving
• A resolution theorem prover for intuitionistic logic
• Satisfiability of High-Level Conditions
• Resolution-based theorem proving for many-valued logics
• Resolution theorem proving in reified modal logics
• scientific article; zbMATH DE number 4128784
• Theorem proving by chain resolution

Cites work

• scientific article; zbMATH DE number 1701353 (Why is no real title available?)
• scientific article; zbMATH DE number 1809861 (Why is no real title available?)
• scientific article; zbMATH DE number 1231489 (Why is no real title available?)
• scientific article; zbMATH DE number 1142315 (Why is no real title available?)
• scientific article; zbMATH DE number 194642 (Why is no real title available?)
• A Logic of Graph Constraints
• A Machine-Oriented Logic Based on the Resolution Principle
• An algorithm for approximating the satisfiability problem of high-level conditions
• Attributed Graph Constraints
• Correctness of high-level transformation systems relative to nested conditions
• Formal Methods in Software and Systems Modeling
• Fundamentals of algebraic graph transformation
• Graph-based specification of access control policies
• Modeling and verifying graph transformations in proof assistants
• Theory of constraints and application conditions: from graphs to high-level structures
• Weakest Preconditions for High-Level Programs

Cited in

(12)

• A navigational logic for reasoning about graph properties
• scientific article; zbMATH DE number 7453970 (Why is no real title available?)
• Institutions for navigational logics for graphical structures
• Theorem proving graph grammars with attributes and negative application conditions
• Interactive and automated proofs for graph transformations
• Reasoning with graph constraints
• Rewriting theory for the life sciences: a unifying theory of CTMC semantics
• Symbolic graphs for attributed graph constraints
• On the Specification and Verification of Model Transformations
• Analysis of graph transformation systems: native vs translation-based techniques
• Satisfiability of High-Level Conditions
• An algorithm for approximating the satisfiability problem of high-level conditions

Describes a project that uses

Uses Software

• VAMPIRE

This page was built for publication: Resolution-Like Theorem Proving for High-Level Conditions

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3540406)