Lab for Automated Reasoning and Analysis LARA

Lecture 19

(Presented by Ruzica Piskac.)

Push-down automata

Equivalence of push-down automata and context-free grammars.

Intersection of a regular and context-free language.

First-order theorem provers

Completeness of propositional resolution.

Undecidability of first-order logic.

Completeness of first-order resolution.


sav07_lecture_19.txt · Last modified: 2007/05/31 12:14 by vkuncak