清洗
发表于 2025-3-23 10:46:58
From action calculi to linear logic,li using the propositions-as-types paradigm; the type theory has a sound and complete interpretation in Power‘s categorical models. We go on to give a sound translation of our type theory in the (type theory of) intuitionistic linear logic, corresponding to the relation between Benton‘s models of li
essential-fats
发表于 2025-3-23 15:57:11
http://reply.papertrans.cn/24/2338/233765/233765_12.png
muster
发表于 2025-3-23 19:12:13
Linear lower bounds and simulations in frege systems with substitutions,nd using Kolmogorov Complexity we give a more general framework to obtain superlogarithmic lower bounds for the number of lines in both tree-like and dag-like .. We show the previous known lower bound, extend it to the tree-like case and, for another class of tautologies, we give new lower bounds th
骂人有污点
发表于 2025-3-23 23:03:14
http://reply.papertrans.cn/24/2338/233765/233765_14.png
加强防卫
发表于 2025-3-24 03:41:08
,A proof-theoretical investigation of Zantema’s problem, of the string-rewriting system 1100 → 000111. This rewriting system is self-embedding, so the standard termination techniques which rely on Kruskal‘s Tree Theorem cannot be applied directly. Dershowitz and Hoot have given a classical termination proof using a minimal bad sequence argument. We a
Ankylo-
发表于 2025-3-24 08:46:43
Spectra with only unary function symbols,ges that contain only unary function symbols. In particular, it is shown that a set . of natural numbers is the spectrum of a sentence over the language of one unary function symbol precisely if . is an eventually periodic set.
包庇
发表于 2025-3-24 12:50:50
Classical proofs via basic logic,ch has been extended to classical logic (cf. Girard 1991, Parigot 1991, and recently Danos Joinet Schellinx 1997). This paper introduces a new sequent calculus for (propositional) classical logic, indicated by .C. Both, the calculus and the cut-elimination procedure for .C extend those for . (Sambin
Respond
发表于 2025-3-24 15:32:47
Full abstractness for a functional/concurrent language with higher-order value-passing, for processes; the constructors for terms of this type are similar to those found in standard process calculi such as CCS. We first give an operational semantics for this language in terms of a labelled transition system which is then used to give a behavioural preorderbased on contexts; the expres
暂时休息
发表于 2025-3-24 19:45:58
http://reply.papertrans.cn/24/2338/233765/233765_19.png
sterilization
发表于 2025-3-25 02:28:14
A mixed modal/linear lambda calculus with applications to bellantoni-cook safe recursion,ated with modality and linearity are avoided. We study the basic metatheory of this system including existence and inference of principal types..The system serves as a platform for certain higher-order generalisations of Bellantoni-Cook‘s function algebra capturing polynomial time using a separation