Liste des Groupes | Revenir à s logic |
On 2024-05-27 14:15:57 +0000, olcott said:<snip>
On 5/27/2024 3:00 AM, Mikko wrote:
Minimal Type Theory (YACC BNF)That is not far from useful. Much of the code could be reused forUsers of your MTT basically need two programs: one that checks whether>
the input is syntactiaclly correct and identifies at least one error
if it is not, and one that checks whether a proof (that may but need
not have unproven premises) is valid and identifies at least one error
if it is not.
>
MTT is build with YACC and LEX and outputs the XML of the
input expression.
>
LP := ~True(L, LP)
>
definition_2 token="ASSIGN_ALIAS"
| definition_2 token="IDENTIFIER" value="LP"
| sentence_2 token="NOT"
| | atomic_sentence_1 token="IDENTIFIER" value="True"
| | | term_list_1
| | | | term_2 token="IDENTIFIER" value="L"
| | | | term_2 token="IDENTIFIER" value="LP"
>
Directed graph of evaulation sequence of LP
Nodes on the left edges on the right
00 NOT 01
01 True 02, 00 // cycle
02 L
>
<definition_2 token="ASSIGN_ALIAS">
<definition_2 token="IDENTIFIER" value="LP"/>
<sentence_2 token="NOT">
<atomic_sentence_1 token="IDENTIFIER" value="True">
<term_list_1>
<term_2 token="IDENTIFIER" value="L"/>
<term_2 token="IDENTIFIER" value="LP"/>
</term_list_1>
</atomic_sentence_1>
</sentence_2>
</definition_2>
the more useful programs mentioned above.
Les messages affichés proviennent d'usenet.