## Overview of Automated Reasoning

author: Peter Baumgartner, Australian National University
published: April 1, 2009,   recorded: January 2009,   views: 812
Categories
You might be experiencing some problems with Your Video player.

# Slides

0:00 Slides Automated Theorem Proving Purpose of This Lecture Part 1: What is Automated Theorem Proving? First-Order Theorem Proving in Relation to ... Logical Analysis Example: Three Coloring Problem Three Coloring Problem - Graph Theory Abstraction Three Coloring Problem - Formalization Three Coloring Problem - Solving Problem Instances ... - Example 1 Three Coloring Problem - Solving Problem Instances ... Three Coloring Problem: The Role of Theorem Proving - Example 2 Three Coloring Problem: The Role of Theorem Proving - Another Example: Proving Symmetries - Example 3 - Another Example: Proving Symmetries Part 2: Methods in Automated Theorem Proving How to Build a (First-Order) Theorem Prover (1) How to Build a (First-Order) Theorem Prover (2) Languages and Services — Propositional SAT DPLL as a Semantic Tree Method (1) DPLL as a Semantic Tree Method (2) DPLL as a Semantic Tree Method (3) DPLL as a Semantic Tree Method (2) DPLL as a Semantic Tree Method (3) DPLL as a Semantic Tree Method (4) DPLL as a Semantic Tree Method (5) DPLL as a Semantic Tree Method (3) DPLL as a Semantic Tree Method (5) Languages and Services — Description Logics

# Report a problem or upload files

If you have found a problem with this lecture or would like to send us extra material, articles, exercises, etc., please use our ticket system to describe your request and upload the data.
Enter your e-mail into the 'Cc' field, and we will keep you updated with your request's status.

Part 1 55:48
!NOW PLAYING

Part 2 48:17

Part 3 31:08

Part 4 1:01:48

# Description

Course Description:In many applications, we expect computers to reason logically. We might naively expect this to be what computers are good at, but in fact they find it extremely difficult. In this overview course, we look briefly at several varieties of mechanical reasoning. The first is automated deduction, whereby conclusions are derived from assumptions purely by following an algorithm, without user intervention. Automated deduction procedures are parametrized by the logic they are capable of reasoning with. We distinguish between propositional logic and first-order logic. Development and application of propositional logic procedures, also called SAT solvers, received considerable attention in the last ten years, e.g., for solving constraint satisfaction problems, applications in hardware design, verification, and planning and scheduling. Regarding automated deduction in first-order logic, we discuss applications, standard deductive procedures such as resolution, and basic concepts, such as unification. We also examine the dual problem of theorem proving, viz., generating models of a given theory, which has applications to finding counterexamples for non-theorems. A third important area covered in the course is dealing with interactive theorem proving. Interactive theorem proving requires certain amount of instructions from the user to tell the proving program (the theorem prover) how to proceed with a proof. Such interaction is required usually because of the use of higher-order logics, whose expressive formalisms allow natural modeling of complex systems, such as operating system or various protocols. A recent trend in the development of interactive proving is to improve its automation, by combining the power of automatic provers.