Logic Programming

• Text: "First-Order Logic and Automated Theorem Proving"
  • Author:Melvin Fitting
  • Publisher: Springer-Verlag
  • ISBN:0-387-94593-8

Class news group ("drexel.cs.class.logic-prog")

This course will explore the theory and applications of logic programming.

Prerequisites: A knowledge of first-order logic and the Prolog language.

There will be two hour-long exams and occasional mini-programming projects.

• Overview of Logic programming and its applications.
• Overview of logic. Review of Prolog.
• Propositional calculus and proof-techniques.
  • Normal forms: clause form and dual clause form.
  • Algorithms for putting sentences in normal form (Prolog).
• Semantic Tableaux and Resolution.
  • Refutation systems.
  • Propositional tableaux.
  • Propositional tableaux implementations (Prolog).
  • Propositional resolution.
  • Soundness and completeness (Hintakka's Lemma).
  • Other propositional proof techniques.
• First-Order Logic.
  • Syntax and semantics.
  • Models.
  • Proof techniques.
    • First-Order Semantic Tableaux.
    • Unification.
    • First order resolutions (connections with the Prolog language).
    • Tableaux Implementations (Prolog).
• Applications.
  • Logic problems.
  • Proving program correctness.

Microcomputer implementations of Prolog (for downloading):

• MacOS
• Windows

Automated Deduction on the Web

Otter Home Page

List of Logic programming applications in industry

Microcomputer implementations of Otter(for downloading)

• MacOS
• DOS
• Windows 95

Notes on using Otter