🛠 七月最新开发更新 – 构建Tau Net的TestNet Alpha核心 团队在完成区块创建、提高解析性能和开发公式归一化的新算法方面，进一步推进了TestNet Alpha的进展。 亮点： - TestNet Alpha：区块创建、链接和Merkle根存储已完成 - SAT求解器：从Z3迁移到CVC5，解锁了更好的归一化和可满足性 - 解析引擎：性能提升60% + 潜在的新解析专利 - 语言研发：反前束归一化和布尔量词消除规范已准备好。 Ohad一直在审查最新的时态逻辑论文。Tau Net和$AGRS在该领域的学术进展上仍然遥遥领先。 时间戳： 00:12 - Karim的总结 03:48 - David（首席开发者） - 成功从Z3切换到CVC5，改善了整体求解器性能。 - 完成了CVC5的归一化、可满足性和解释器模块的工作。 - 实施了Ohad建议的推迟字面解析的位向量方程方法。 - 协助Umar进行代码审查和调试。 05:36 - Lucca（Tau语言开发者） - 开发了消除函数量词的算法初步规范，以用于Tau的表格功能。 - 将其集成到反前束归一化算法中，以处理CVC5未覆盖的公式。 - 伪代码已最终确定，准备实施该算法。 - 开始使用Tomáš的新树实现，并协助解决其最终问题。 08:30 - Andrei Korotkoff（高级开发者） - 完成了区块生产和存储的testnet alpha里程碑，包括内存池处理、区块链接、Merkle根计算和数据库持久性。 - 这项工作为下一个里程碑奠定了基础：基于区块历史的持久链状态。 - 开发了一个复杂的负载测试工具，以模拟Tau解释器行为和区块链动态在逐点修订下的表现。 11:20 - Tomáš Klapka（高级开发者） - 修复了树切换中的几个问题，包括否定处理、语法错误和类型推断错误。 - 将解析器库重构为仅头文件。 - 为TGF工具和解析器创建了Docker支持和夜间发布。 - 更新了Tau语言以集成改进的解析器。 12:26 - Ohad（创始人兼CTO） - 专注于新算法设计和团队协作。 - 探索领域无关语言以增强决策程序。 - 审查了最近的时态逻辑学术论文，并确认Tau在当前研究中仍然处于领先地位。