Speaker: |
Ashutosh K. Gupta (Institute of Science and Technology, Austria Am Campus 1 3400 Klosterneuburg Austria) |

Date: |
Friday, 12 Oct 2012, 15:30 to 16:30 |

Venue: |
A-212 (STCS Seminar Room) |

(Scan to add to calendar)

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.