Interaktiver Theorembeweis (ITP)

- Natural & Formal Sciences -
Mathematics & Logic Dictionary
Definition
Eine Methode zur Erzeugung formaler, maschinengeprüfter Beweise durch Kombination menschlicher Steuerung mit Beweisassistenten und Taktiksprachen zur Konstruktion von Beweisskripten, die ein Prüfer akzeptiert.