-
Notifications
You must be signed in to change notification settings - Fork 1
System Template
List of people involved with the development of the system.
Provide here some general information.
- Proving
- Model finding
Provide here some information about the input expressiveness.
In case the input format is system-specific, provide here the description of the proof format.
In case the input format is shared, link to the existing format page (create one if not available yet). Please indicate derogations and/or extensions of the standard.
Remove comments (tags) of unsupported input formats (and then also remove this line).
How can a user interpret the output of the system easily (top-level perspective)? If you are following a standard (like TPTP SZS or SMT-Lib) just say so. If not, you can provide a table with common outputs (please adjust the following template as you see fit):
| Output | Meaning |
|---|---|
Heureka x! |
The system found a proof for input file x. |
No can do x |
The system did not succeed in establishing any result for input file x. |
Error error |
Something went wrong. |
In case the proof format is system-specific, provide here the description of the proof format.
In case the proof format is shared, link to the existing format page (create one if not available yet). Please indicate derogations and/or extensions of the standard.
In case there are no proofs outputted, please say so too.
Remove comments (tags) of unsupported proof formats (and then also remove this line).
Provide here a link to the tool and its documentation
For instance: where is the tool mainly used? Is it open source? If so, what is the license? System-specific restrictions (e.g., only on Linux). Maybe provide a small usage example...
Either: Maintained or: Archived
If possible, give a list of papers/documents (preferrably via DOIs) that give further details to the system.
Add here a one line description of the tools around the system (e.g. tools to check the specific proof format, tuning tools, evaluation tools, debuggers...) together with a link.
Erase this section if empty.