椭圆
发表于 2025-3-26 23:00:56
Non Commutative Logic: A Survey (Abstract)Noncommutative Logic (NL) has been introduced by Abrusci and Ruet (Non-Commutative Logic I, Annals of Mathematical Logic, 2001). NL is a refinement of Linear Logic (LL) and a conservative extension of Lambek Calculus (LC). Therefore, NL is a constructive logic (i.e. proofs are programs).
掺假
发表于 2025-3-27 04:09:54
Simplification Rules for Constrained Formula TableauxSeveral variants of a first-order simplification rule for non-normal form tableaux using syntactic constraints are presented. These can be used as a framework for porting methods like unit resolution or hyper tableaux to non-normal form free variable tableaux.
边缘带来墨水
发表于 2025-3-27 08:02:48
http://reply.papertrans.cn/17/1664/166333/166333_33.png
tariff
发表于 2025-3-27 12:24:47
https://doi.org/10.1007/978-94-007-0400-8 a generic tableau method which combines features of explicit tableau methods for modal logics with constraint label management and the classical tableau method for first-order logic, and we prove its soundness and completeness.
Grandstand
发表于 2025-3-27 13:47:49
Poh Poh Wong,Lee Boon-Thong,Maggi W.H. Leungre is semantically guided: an interpretation (provided by the user) is used for pruning the search space. This interpretation is refined dynamically during proof search until a model or a contradiction is found. The method has been implemented and some preliminary experimental results are presented.
共和国
发表于 2025-3-27 21:47:53
A General Tableau Method for Propositional Interval Temporal Logics a generic tableau method which combines features of explicit tableau methods for modal logics with constraint label management and the classical tableau method for first-order logic, and we prove its soundness and completeness.
吹牛大王
发表于 2025-3-27 22:18:25
http://reply.papertrans.cn/17/1664/166333/166333_37.png
无能力
发表于 2025-3-28 03:05:57
Automated Theorem Proving in Generation, Verification, and Certification of Safety Critical Code (Abering group at NASA Ames. We are developing automatic program synthesis systems for state estimation and navigation, AutoFilter, and data analysis ( AutoBayes). These tools automatically generate documented C/C++ code from compact, high-level specifications.
搜集
发表于 2025-3-28 06:27:24
Tableaux with Four Signs as a Unified Framework Belnap’s four-valued logic), Nelson’s logics for constructive negation, and da Costa’s paraconsistent logic .. (together with some of its extensions). For the latter we provide new, simple semantics for which our tableau systems are sound and complete.
Gyrate
发表于 2025-3-28 12:37:09
XPath and Modal Logics of Finite DAG‘sbeen studied in hybrid logic by nominals. We add nominals to the modal logic of Palm and interpret the language on directed acyclic graphs. We give an algorithm which decides the consequence problem of this logic in exponential time. This yields a complexity result for query containment of the corresponding extension of XPath.