Current Slide

Automatic theorem proving deals with the design and implementation of computer programmes that are capable of making mathematical proofs.

Theorem provers deduce new formulas from given formulas via logical deduction rules until the target formula is found.

Theoretical foundation of automated theorem proving: mathematical logic; typically first-order-logic.

Formulas are mathematically precisely defined via interpretations (provide semantics for function and predicate symbols via mappings and relations respectively)