dissent
发表于 2025-3-27 00:54:26
https://doi.org/10.1007/978-3-540-92687-0Automat; automated deduction; complexity; game theory; interactive theorem proving; logic; theorem proving
Prosaic
发表于 2025-3-27 04:03:47
http://reply.papertrans.cn/59/5882/588147/588147_32.png
Carbon-Monoxide
发表于 2025-3-27 05:36:59
Logical Foundations of Computer Science978-3-540-92687-0Series ISSN 0302-9743 Series E-ISSN 1611-3349
forbid
发表于 2025-3-27 10:18:52
, with Strategy Contexts and Bounded Memory,milar formalisms (., .*, Game Logic, Strategy Logic, ...). We then address the problem of model-checking for our logics, especially we provide a . algorithm for the sublogics involving only memoryless strategies and an . algorithm for the bounded-memory case.
天然热喷泉
发表于 2025-3-27 14:31:30
http://reply.papertrans.cn/59/5882/588147/588147_35.png
展览
发表于 2025-3-27 19:09:47
http://reply.papertrans.cn/59/5882/588147/588147_36.png
neolith
发表于 2025-3-28 00:34:02
http://reply.papertrans.cn/59/5882/588147/588147_37.png
松果
发表于 2025-3-28 03:28:20
The Logic of Proofs as a Foundation for Certifying Mobile Computation,nstructed out of code components and extant type systems track local resource usage to ensure the mobile nature of these components, our system . ensures correct . out of certificate components. We present proofs of type safety and strong normalization for a run-time system based on an abstract machine.
战胜
发表于 2025-3-28 10:10:28
Games on Strings with a Limited Order Relation,r relation and the usual (linear) order relation, and a finite number of unary predicates. On the basis of such conditions, we outline a polynomial (in the size of the input strings) algorithm to compute the “remoteness” of a game and to determine the optimal strategies/moves for both players.
发誓放弃
发表于 2025-3-28 14:17:32
Hypersequent Systems for the Admissible Rules of Modal and Intermediate Logics, objects of the systems are sequent rules. Here, the framework is extended to cover derivability of the admissible rules of intermediate logics and a wider class of modal logics, in this case, by taking hypersequent rules as the basic objects.