Automated Reasoning – Seminar

Wintersemester 2019/20

Übungsaufgaben:

• Übung 1: Formalisierung in PL1 (Version 1.1 mit mehr Hinweisen).
• Übung 2: Semantik von PL1 .
• Übung 3: Theorembeweisen mit Hets.
• Übung 4: Hornlogik und Gavel, Problem 4.1, Problem 4.2, Problem 4.3, Problem 4.4.
• Übung 5: Horn mit Äquivalenz, Problem 5.1, Problem 5.2, Problem 5.3,

Zusätzliche Materialien

• big.p
• Thousands of Problems for Theorem Provers
• Download (~600 MB)
• Gavel
• Testprobleme:
  • Problems/BIO/BIO002+1.p
  • Problems/NUM/NUM006+1.p
  • Problems/NLP/NLP218+1.p
  • Problems/NLP/NLP261+1.p
  • Problems/SET/SET020+1.p
  • Problems/SET/SET084+1.p
  • Problems/SET/SET093+1.p
  • Problems/SET/SET095+1.p
  • Hinweis: Für die SET-Probeme könnte ein Update von gavel nötig sein.

Aktuelle Informationen:

• Bei Fragen und Problemen wenden Sie sich bitte per E-Mail an den Webmaster.

Webmaster