Skip to content
Snippets Groups Projects
Unverified Commit 17948f05 authored by Colin Rothgang's avatar Colin Rothgang
Browse files

udate cade-2025 folder

parent 5cf95ba2
Branches master
No related tags found
No related merge requests found
Source diff could not be displayed: it is too large. Options to address this: view the blob.
The TPTP problems in the files example_conjecture.p and example_typechecking_obligtion.p are the TPTP translations of the property that function compositions have the expected type and of the associativity of function composition.
Due to the fact that we inline (definition expand) the definitions of function composition and application using plain function application in TPTP, these problems become very simple TPTP conjectures that can be easily solved by all recommended HOL ATPs at https://tptp.org/cgi-bin/SystemOnTPTP.
The 7 recommended systems are listed in the file recommended-systems.txt.
The TPTP system output of the 8 recommended ATPs (run via https://tptp.org/cgi-bin/SystemOnTPTP) for the two problems is listed in the files
example_conjecture__system_outputs.txt and example_typechecking_obligtion__system_outputs.txt.
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment