Proof simplification for model generation and its applications

DOI10.1007/3-540-44404-1_8MaRDI QIDQ2767011zbMATH OpenFDO

Authors Miyuki Koshimura, Ryuzo Hasegawa

Publication date 22 July 2002

Published in Lecture Notes in Artificial Intelligence (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-44404-1_8

Mathematics Subject Classification ID

Recommendations

• Proof simplification in the framework of coherent logic
• Model elimination with simplification and its application to software verification
• Proof simplification and automated theorem proving
• Toward mechanical methods for streamlining proofs
• Simplification of proof procedures based on the path condition concepts

Cited in

(11)

• Simplification of proof procedures based on the path condition concepts
• Simplify: a theorem prover for program checking
• On the convergence of reduction-based and model-based methods in proof theory
• Flexible heuristics for simplification with conditional lemmas by marking formulas as forbidden, mandatory, obligatory, and generous
• Proof simplification in the framework of coherent logic
• An Implementation of the Model Elimination Proof Procedure
• Model elimination with simplification and its application to software verification
• Proof simplification and automated theorem proving
• ILF-SETHEO
• Toward mechanical methods for streamlining proofs
• A versatile, sound tool for simplifying definitions

Describes a project that uses

Uses Software

• SPASS
• TPTP

This page was built for publication: Proof simplification for model generation and its applications

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