🛠 Aggiornamento Sviluppo di Luglio – Costruendo il Core del TestNet Alpha di Tau Net Il team ha fatto ulteriori progressi verso il TestNet Alpha finalizzando la creazione dei blocchi, migliorando le prestazioni di parsing e sviluppando nuovi algoritmi per la normalizzazione delle formule. Punti salienti: - TestNet Alpha: Creazione dei blocchi, collegamento e memorizzazione della radice Merkle completati - SAT Solver: La migrazione da Z3 a CVC5 ha sbloccato una migliore normalizzazione e soddisfacibilità - Motore di Parsing: Aumento delle prestazioni del 60% + potenziale nuovo brevetto per il parsing - R&D Linguistica: Normalizzazione anti-prenexing e specifica per l'eliminazione dei quantificatori booleani pronte. Ohad ha esaminato i più recenti articoli sulla logica temporale. Tau Net e $AGRS rimangono molto avanti rispetto ai progressi accademici attuali nel campo. Timestamp: 00:12 - Riepilogo di Karim 03:48 - David (Sviluppatore Capo) - Passato con successo da Z3 a CVC5, migliorando le prestazioni complessive del solver. - Completato il lavoro sulla normalizzazione, soddisfacibilità e moduli interpreti con CVC5. - Implementato l'approccio suggerito da Ohad di rinviare la risoluzione letterale per le equazioni a vettore di bit. - Assistenza a Umar con revisioni del codice e debugging. 05:36 - Lucca (Sviluppatore Linguaggio Tau) - Sviluppata la specifica iniziale per un algoritmo per eliminare i quantificatori di funzione da utilizzare nella funzione tabella di Tau. - Integrato nell'algoritmo di normalizzazione anti-prenexing per gestire formule non coperte da CVC5. - Preparandosi a implementare questo algoritmo ora che il pseudo-codice è finalizzato. - Iniziato a utilizzare la nuova implementazione ad albero di Tomáš e assistito nella risoluzione dei suoi problemi finali. 08:30 - Andrei Korotkoff (Sviluppatore Senior) - Completato il traguardo del testnet alpha per la produzione e memorizzazione dei blocchi, inclusa la gestione della mempool, collegamento dei blocchi, calcolo della radice Merkle e persistenza del database. - Questo lavoro getta le basi per il prossimo traguardo: stato della catena persistente basato sulla cronologia dei blocchi. - Sviluppato uno strumento complesso di test di carico per simulare il comportamento dell'interprete Tau e le dinamiche della blockchain sotto revisione puntuale. 11:20 - Tomáš Klapka (Sviluppatore Senior) - Risolti diversi problemi derivanti dal passaggio all'albero, inclusa la gestione della negazione, errori di grammatica e di inferenza di tipo. - Rifattorizzata la libreria del parser per essere solo header. - Creata la supporto Docker e rilasci notturni per lo strumento TGF e il parser. - Aggiornato il linguaggio Tau per integrare il parser migliorato. 12:26 - Ohad (Fondatore & CTO) - Concentrato sulla progettazione di nuovi algoritmi e sulla collaborazione del team. - Esplorati linguaggi indipendenti dal dominio per migliorare le procedure decisionali. - Rivisti articoli accademici recenti sulla logica temporale e confermato che Tau rimane avanti rispetto alla ricerca attuale.