You are here: Home Kolloquium Automatic Reasoning: Achievements and Challenges

Automatic Reasoning: Achievements and Challenges

Prof. Dr. Christoph Weidenbach, Max-Planck-Institut für Informatik

Event details
    When Nov 20, 2019
    from 16:00 to 18:00
    Where Hörsaal 7, Endenicher Allee 19c, 53115 Bonn
    Add event to calendar vCal
    For SAT, propositional satisfiability testing, the CDCL (Conflict Driven Clause Learning) calculus is currently considered to be the prime calculus. It has changed the way hardware is developed. For SMT, satisfiability testing modulo theories, the Nelson-Oppen theory combination procedure together with CDCL is currently considered to be the prime calculus. It has changed the way software is automatically analyzed. Both approaches, CDCL and SMT, are dedicated to logics without first-order logic variables. The introduction of first-order logic variables extends the applicability of the resulting logic to the level of highly expressive knowledge representation formalisms. I will first show why SAT and SMT work in practice and then discuss that the introduction of first-order variables implies the non-existence of a single prime calculus in the spirit of SAT or SMT. This holds already for decidable fragments of first-order logic extended with theories. Instead, different calculi based on the instantiation of variables, the approximation of formulas, an explicit partial model building, an implicit partial model building, and syntactic inference restrictions and combinations thereof need to considered for the next step towards machine intelligence based on logical reasoning.

    Document Actions