Research Institute for Symbolic Computation (RISC-Linz)

Johannes Kepler University

A-4040 Linz, Austria, Europe

URL: http://www.risc.uni-linz.ac.at/people/tjebelea

Phone: +43 732 2468 9946

Fax: +43 732 2468 9930

Tudor.Jebelean@JKU.AT

Subjects from previous examinations: tsw-exam-1.pdf, tsw-exam-2.pdf, tsw-exam-3.pdf.

Subjects with solutions: tsw-exam-sol-1.pdf.

- Proof example for using negation: proof-example.pdf.
- Study of the algorithm for reversing a list: reverse.pdf,

- Introduction: Working-Techniques-1-Intro-2008-08-28-21h26.ppt
- Basic proof techniques: Buchberger-Proof-Techniques.pdf
- Proof techniques and examples of proofs: Buchberger-Proofs-in-Predicate-Logic.pdf
- Definitions in predicate logic: Buchberger-Logic-Definitions.pdf
- Reading: Working-Techniques-2-Reading-2008 2008-08-29-14h35.ppt
- Speaking and Writing:

** All this material is copyrighted by Bruno Buchberger and it may be used
only by the students participating in this lecture and for the purpose of
studying for this lecture.**

- "Automated Theorem Proving" by Tudor Jebelean: Jebelean-ATP.pdf
- Short programming example by Tudor Jebelean: reverse.pdf
- Proof example by Tudor Jebelean: proof-example.pdf

- Programming using rewriting Mma-programs.pdf.
- Alternative model of propositional logic propositional.pdf
- Imperative program verification by symbolic execution symbolic-execution-paper.pdf
- Lecture notes on Computational Logic by Adrian Craciun: home page.
- Logic for Computer Science by Bruno Buchberger: Buchberger-Logic-for-Computer-Science.pdf.
- Deduction in natural style by Tudor Jebelean: Jebelean-Natural-Deduction.pdf

T. Jebelean