Christoph Weidenbach
The Design of Automated Reasoning Systems
VCLA will be hosting a talk by Christoph Weidenbach on May 23rd, 2013.
| DATE: | Tuesday, June 4, 2013 |
| TIME: | 10:00 |
| VENUE: | von Neumann seminar room |
ABSTRACT
An automated reasoning system is the combination of a problem, its model in a logic, the applied calculus and the implementation of the calculus in software. By examples as well as theoretical insights I will in particular argue that for the design of an adequate calculus the dimensions of inference rules, simplification and reduction rules, theory support, ordering restrictions, and partial model assumptions have to be nicely composed. Considered problems will come from industry and computer science, considered logics range from propositional to predicate logic with arithmetic, calculi from CDCL to hierarchic superposition and implementations from SAT solvers to theorem provers.
