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

Evaluation

To pass, there are the following preconditions
max. 3 missed exercises
min. 12 points from homeworks
min. 15 points from the final exam

6 homeworks, open 24 hours. 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)

3 examples - resolution; tableaux proofs in propositional logic (24 p.) October 21 D1
Questionnaire (12 p.) Nov. 25, 8 a.m. D1

Extra points

Final exam (duration 75 min, 40 p.)
Thu Dec 17, 16:00. B204; Wed Jan 6 12:00, Wed Jan 13. 14:00, Tue Jan 19. 16:00

Reading

September 23: Resolution in propositonal logic
(Nerode, Shore, pp. 49-62, see Study materials, Reading in IS MU)
September 30: DPLL
(Davis-Putnam-Logemann-Loveland Procedure, in Stanford Encyclopedia of Philosophy, Automated Reasoning Section 4.2)
and slides of this course.
October 7
Datalog. Query Processing in Deductive DB. See Study materials, Reading in ISMU
Recommended: Executable Knowledge.
October 14
Automated Reasoning Section 4. In Stanford Encyclopedia of Philosophy.
Overview of Automated Reasoning by Peter Baumgartner (at SSLI 2009)
November 4
Automated Reasoning Section 2: Deduction Calculi.
The Problem of Induction, up to 4.0. In Stanford Encyclopedia of Philosophy.
December 2
Libor Běhounek, Many-valued logics. Reading in ISMU
Natural Logic Inference for Common Sense Reasoning. Reading in ISMU
(Not obligatory, only for fans: Montague semantics. In Stanford Encyclopedia of Philosophy.)
December 9
Negation and Nonmonotonic Logic. Reading in ISMU
The Certainty-Factor Model
Description Logic and Logics

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 (2.5 lessons)
  • Propositional logic. Resolution (pdf)
  • Predicate logic. Resolution (pdf) (animation)
  • On satisfiability (pdf)
  • SAT problem. Davis-Putnam Algorithm (pdf) Animation
    DPvis Visualizing Davis-Putnam Procedure
• Deduction (1 lesson)
  Tableau Proofs (ps) (pdf) (ps 4 pages) (Atomic tableaux)
  Animations for propositional and predicate logic.
  LeanTAP, SWI Prolog implementation of a tableau prover
• Prolog and inference (1 lesson)
  • Logic programming and Prolog (ps) (pdf) (ps 4pages)
  • Box model. Metainterpreters (ps) (pdf) (ps 4pages)
    
  • Deductive databases and Datalog (intro) (datalog) (In Encyclopedia of Database Systems)
  • Knowledge-based systems (pdf)
    
  • Backward chaining. Forward chaining (pl)
• Inductive inference (2 lessons)
  Logical consequence and
  Inductive inference in propositional logic (ppt)
  Classification (ppt)
  Version spaces (Animation)
  Decision tree learning (Animation I) (Animation II)
  Inductive logic programming I (pdf) (pdf) II (pdf)
  Inverse resolution by Naren Ramakrishnan
  Inductive synthesis of logic programs
  Model Inference Problem and Model Inference System (Ehud Shapiro) (here)
  Assumption-based reasoning (ps) (pdf) and assumption-based learning (slides) (session) and details (here)
  Learning frequent patterns
• Modal logic
  Introduction
  Cripke frames and tableau proofs (ps) (pdf) (ps 4 pages)
  Atomic tableaux (Animation)
  Slides on Modal Axioms and special Accessibility Relations and some extension notes
  Temporal logics
  Inductive inference in spatiotemporal logic (pdf)
• Non-classical logic, knowledge representation and reasoning (2 lessons)
  Non-classical logics at fiit stu (lecture 9 and 10)
  Inference II. Reasoning with uncertainty
  Overview of (Mycin). Certainty factor : How to work with. More on CF can be found (here)
  
  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, see ISMU, Study materials.
  Semantic Web etc. Tutorials
  RDF, Fresnel (Display Vocabulary for RDF)
  OWL, OIL, DAML+OIL
• Present and future of computational logic (1 lesson)
  Multi-agent systems Book on Decision procedures
  Automated Reasoning: Sequent deduction. Natural deduction. In Stanford Encyclopedia of Philosophy
  

Lógica computacional F.Sci U. Porto
Applied Logic at Cornell
Jiří Raclavský
Logical Methods in Computer Science Journal
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