只有
发表于 2025-3-27 00:49:58
Saturation Up to Redundancy for Tableau and Sequent Calculi,for classical first-order logic. This technique can be used to easily show the completeness of optimized calculi that contain destructive rules e.g. for simplification, rewriting with equalities, etc., which is not easily done with a standard Hintikka-style completeness proof. The notions are first
GLADE
发表于 2025-3-27 03:29:58
Branching-Time Temporal Logic Extended with Qualitative Presburger Constraints,ty and model-checking problem. This language allows to compare the variables at different states of the model and include periodicity constraints, comparison constraints, and a restricted form of quantification. On the other hand, the . counterpart of this logic (and hence also its . counterpart whi
符合规定
发表于 2025-3-27 05:18:23
Combining Supervaluation and Degree Based Reasoning Under Vagueness,on with respect to precisification spaces, which consist in collections of classical interpretations that represent admissible ways of making vague atomic statements precise. On the other hand, .-norm based fuzzy logics model truth functional reasoning, where reals in the unit interval are int
Bravura
发表于 2025-3-27 09:34:15
A Comparison of Reasoning Techniques for Querying Large Description Logic ABoxes,ntologies. For such applications, we conjectured that reusing ideas of deductive databases might improve scalability of DL systems. Hence, in our previous work, we developed an algorithm for reducing a DL knowledge base to a disjunctive datalog program. To test our conjecture, we implemented our alg
不合
发表于 2025-3-27 14:40:15
A Local System for Intuitionistic Logic,e that, in applying the rules of the system, one needs only a fixed amount of information about the logical expressions involved. The main source of non-locality is the contraction rules. We show that the contraction rules can be restricted to the atomic ones, provided we employ ., i.e., to allow ru
柔软
发表于 2025-3-27 21:23:16
CIC,: Type-Based Termination of Recursive Definitions in the Calculus of Inductive Constructions,cations that type-based termination provides an appropriate foundation for proof assistants based on type theory; however, most work to date has been confined to non-dependent type systems. In this article, we introduce a variant of the Calculus of Inductive Constructions with sized types and study
手铐
发表于 2025-3-27 22:07:04
http://reply.papertrans.cn/59/5881/588013/588013_37.png
incredulity
发表于 2025-3-28 06:07:44
978-3-540-48281-9Springer-Verlag Berlin Heidelberg 2006
angiography
发表于 2025-3-28 06:45:22
Logic for Programming, Artificial Intelligence, and Reasoning978-3-540-48282-6Series ISSN 0302-9743 Series E-ISSN 1611-3349
Ingratiate
发表于 2025-3-28 10:29:28
http://reply.papertrans.cn/59/5881/588013/588013_40.png