| Description |
Various verification methods depend on theorem provers to obtain proofs of verification conditions. If the provers return proofs that satisfy certain structure then it may enhance the performance of the verification methods. Theorem provers aim to find the proofs using the most efficient algorithms. Therefore, the returned proofs from the existing theorem provers may not satisfy such structures. In my talk, I will present two pieces of our work that transform the proofs produced by the provers to obtain such structured proofs.
In the first work, we present a new efficient parametrized method to remove redundant parts of resolution proofs. The parameter allows one to choose between coverage of the redundancy removal and the efficiency of the method.
In the second work, we present a set of proof transformation rules that obtains "localize proofs" from proofs of unsatisfiable formulas. The localize proofs allow one to compute (tree)-interpolants efficiently.
|