Small screen detected. You are viewing the mobile version of SlideWiki. If you wish to edit slides you will need to use a larger device.
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)
This work is licensed under a Creative Commons Attribution-ShareAlike 4.0 International License