Computational Logic

CZ.1.07/2.2.00/28.0209 Elektronické opory a e-learning pro obory výpočtového a konstrukčního charakteru

To pass, there are four preconditions
to write introductory test and final test
max. 3 absences for exercises
min. 12 points from homeworks
min. 25% points from the final exam

6 homeworks, open on Mondays. Two trials, the better is counted. Max. 4 p. per homework,
answer correct/incorrect/missing 1 unit /-0.5 unit /-0.25 unit, and
unit=4/NumberOfQuestions where NumberOfQuestions can vary (mostly between 10 and 20 per the homework)

1. introductory (in the 1st exercises, necessary to write, no points to the evaluation);
2. supervised (at a lecture time) Nov 13
3. final (in the last exercises, necessary to write, no points to the evaluation)

2 examples - a tableaux proof and maybe something else. Nov 13

Final exam (40 p.)

Anil Nerode, Richard A. Shore. Logic for Applications
Shan-Hwei Nienhuys-Cheng, Ronald de Wolf. Foundations of Inductive Logic Programming
Graham Priest. An Introduction to Non-Classical Logic
Encyclopedia of database systems (Datalog, Executable knowledge). Accesible form FI MU computer networks or via proxies. For more info see MU Libraries web page, Electronic Information Sources.

D. Gabbay, C. Hogger, J.A.Robinson. Handbook of Logic in Artificial Intelligence and Logic Programming
Luc De Raedt. Logical And Relational Learning
Graham Priest. Logic: A Very Short Introduction (Logika. Pruvodce pro każdého)

• Introduction (pdf)

• Prerequisities. Resolution. Flavour of Prolog (1 lesson)
  • Propositional and predicate logic (pdf)
  • On satisfiability (ps) (pdf) (ps 4 pages).
    Resolution in predicate logic (pdf) (animation)
  • SAT problem. Davis-Putnam Algorithm (pdf) Animation
    DPvis Visualizing Davis-Putnam Procedure
  • Logic programming and Prolog (ps) (pdf) (ps 4pages)
• Prolog and inference (1 lesson)
  • Box model. Metainterpreters (ps) (pdf) (ps 4pages)
    Backward chaining. Forward chaining (pl)
  • Knowledge-based systems (pdf)
    Mycin
    The Certainty-Factor Model
    Certainty factor. How to
    
  • Multi-agent systems
  • Readings:
    Book on Decision procedures
    Automated Reasoning: Sequent deduction. Natural deduction. In Stanford Encyclopedia of Philosophy
    Executable knowledge. In Encyclopedia of database systems
  • And more (not for an exam): Overview of Automated Reasoning by Peter Baumgartner (at SSLI 2009)
• Deduction (1 lesson)
  Deductive databases and Datalog (intro) (datalog)
  Tableau Proofs (ps) (pdf) (ps 4 pages)
  Animations for propositional and predicate logic.
  LeanTAP, SWI Prolog implementation of a tableau prover
  Readings:
  Automated Reasoning: Applications
  Datalog. In Encyclopedia of Database Systems
• Induction (3 lessons)
  Inductive inference in propositional logic (ppt)
  Classification (ppt)
  Version spaces (Animation)
  Decision tree learning (Animation I) (Animation II)
  Inductive logic programming I (pdf) II (pdf)
  Inverse resolution by Naren Ramakrishnan
  Inductive synthesis of logic programs
  Model Inference Problem
  Model Inference System (Ehud Shapiro)
  Assumption-based reasoning (ps) (pdf) and assumption-based learning (here)
  Learning frequent patterns
• Non-classical logic, knowledge representation and reasoning (2 lessons)
  Modal logic and Tableau proofs (ps) (pdf) (ps 4 pages) (Animation)
  Temporal logics
  Non-classical logics at fiit stu (lecture 9 and 10)
  Inference II. Reasoning with uncertainty
  Logics for spatial and spatiotemporal data
  Inductive inference in spatiotemporal logic (ps) (pdf)
  Non-monotonic reasoning (in Study materials IS MU -> Non-monotonic logic)
  Brief intro in Stanford Encyclopedia of Philosophy
• Logic for natural language processing (1 lesson)
  • Introduction to NLP
  • Representing text in Prolog
  • Definite Clause Grammars(dcg.pl)
  • Transformation-based tagger
  • Constraint grammars
  • Multirelational learning of a part-of-speech tagger
• Description logic and Semantic web (1 lesson)
  Description Logic
     Franz Baader. The Description Logic Handbook: Theory, Implementation and Applications. Cambridge University Press, 2007. ISBN-13: 978-0521781763.
     Enrico Franconi's course and other courses
  Intro to Semantic Web
  RDF, Fresnel (Display Vocabulary for RDF)
  OWL, OIL, DAML+OIL
• Present and future of computational logic (1 lesson)

Is there a Logic of Exploratory Data Analysis?
Committee on Logic Eduction of Association for Symbolic Logi
Logic Tutorials and Animations
Encyclopedia of Database Systems
summa logicae
Computational Logic Univ. of Madrid
V. Svejdar, Logika: neuplnost, slozitost a nutnost Academia 2002

Mathematical modal logic. A view of its evolution
Temporal Logic Stanford Encyclopedia fo Philosophy
Temporal Logic by Yde Venema
Notes on games in temporal logic by Ian Hodkinson
Linear-time Temporal Logic
Non-classical logics: theory and applications by Esko Turunen, Tampere University of Technology, Finland

Artificial Intelligence by Alison Cawsey at Heriot Watt
ACM Transactions on Computational Logic Scope of the Journal
Advanced Artificial Intelligence (uiowa)
Logic of learning by Peter Flach
Inductive inference and Kolmogorov complexity by Li and Vitanyi
John Lloyd
Knowledge Representation and Reasoning, Univ. of Leeds
Stanford Encyclopedia of Philosophy
Qualitative Spatial Reasoning in Univ. Leeds
J. Ullman's courses
Prover9 and Mace4 Prover9 is an automated theorem prover for first-order and equational logic, and Mace4 searches for finite models and counterexamples. Prover9 is the successor of the Otter prover.
Foundational Ontology by Brandon Bennett
Macintosh Software for Logic and Branden Fitelsen's web site
John McCarthy
CL in Stanford A rigorous introduction to logic from a computational perspective. The course covers propositional logic and relational logic. Topics include syntax, semantics, models, logical entailment, proofs, soundness, completeness, and decidability. Reasoning methods include the truth table method, natural deduction, the Davis-Putnam procedure, resolution, model elimination, demodulation, and paramodulation.
Logics for knowledge representation and reasoning
SAT @ Delft This site contains various sorts of documented research, focused around the satisfiability area, which was carried out at Delft University

Czech version, old and incomplete