The purpose of this work is to study, formally, the provability of implicative formulas by static analysis. To do that, we propose heuristics that allow us to know whether a given formula is satisfiable or not before attempting the proof. The method consists in characterizing the input formula and the program under consideration by mathematical (in)equations representing sufficient conditions for a proof to succeed, if it exists. We are also interested in the analysis and correction of faulty conjectures, especially when correction involves finding a collection of hypotheses, together with a set of axioms, that turn faulty formulas into theorems. The method is based on corrective predicates invention.
we propose a method that can allows us to apply induction hypothesis.
Disclaimer In his capacity as the website owner and because of the full permissions that he has, all of the contents of the faculty member’s website including texts, images, researches and any other media are his responsibility. Therefore, the university disclaim any responsibility on this regard.
Copyright © Deanship of IT & Distance Learning 2018, 1440 H