TU Wien Informatics

20 Years

The Design of Automated Reasoning Systems

  • 2013-06-04
  • Research

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.

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.

Speakers

  • Christoph Weidenbach, Max Planck institut für Informatik, Saarbrücken, Germany

Curious about our other news? Subscribe to our news feed, calendar, or newsletter, or follow us on social media.

Note: This is one of the thousands of items we imported from the old website. We’re in the process of reviewing each and every one, but if you notice something strange about this particular one, please let us know. — Thanks!