辅助变元之于命题与量化布尔公式的作用

使用辅助变元来引入定义,在知识表达中是一个流行和有力的技巧,能够得到更短、更自然的编码而无需冗长的重复。这篇论文中,我们形式地定义了辅助变元的概念,检验了其表达力并讨论了有趣的相关应用。我们把以下两者联系起来:一是,反复使用中间结果而不通过定义重复;二是,布尔函数其他表达中的相似概念。特别的,我们表明带定义的命题逻辑与具有任意输出端的布尔线路以及约束变元满足Horn性质的存在量化布尔公式(记作(?)HORN~b)具有相同的表达力。本文还考虑了定义结构的限制,以及命题定义的扩充。特别的,我们检验了正命题定义与带存在量化的正定义之间的关系(或等价地,检验了(?)HORN~b公式和约束变元未被Horn限定的存在量化的CNF公式(记作(?)CNF~*)之间的关系)。对命题定义的进一步扩充,是允许在定义中使用任意的量词,或等价地,允许布尔公式的嵌入。我们还证明了,量化CNF公式中的约束变元的表达力,是由子句中被约束部分的极小不可满足子公式或极小假子公式的结构所决定的。     

层次图(混合Horn)公式的部分极大可满足性

本文为解决一类混合Horn公式([13,14]),又称为层次图公式([15])的MAXSAT问题进行了基于随机局部搜索过程的经验研究。具体地,我们首先在随机CNF公式的MAX2SAT及MAX3SAT问题上进行WalkSAT和Tabu-Sat(及其变种)的比较,其次,我们在层次图公式上比较了上述过程的改进版本,这些公式编码了随机生成层次图的最小化跨边问题。本文所引入的Tabu-Sat过程,当在搜索空间中检测到一个圈的时候,动态地改变Tabu长度参数。另一个被称为Vector-Tabu-Sat的过程,对所有的布尔变元进行独立的Tabu长度参数管理。一些数值实验的结果显示,我们改进的Tabu-Sat变种在子句个数增长的时候优于Walksat.     

每一个非零的可计算可枚举强有界图灵度都具有反成杯性质

可计算Lipschitz图灵归约（c1-归约）是指用函数被x→x＋c约束的图灵归约,其中c是常数;而ibT归约则通过限制用函数为恒等函数得到。我们通称c1-,ibT-归约为强有界图灵归约。我们证明：对于r=cl,ibT,在可计算可枚举r-度构成的偏序结构（Rr,≤）中,每一个非零的a都具有反成杯性质。为此,我们证明一个新结论：对于每一个不可计算的可计算可枚举集合A,都存在一个不可计算的可计算可枚举B,使得对所有满足A≤wtt C的可计算可枚举集合C都有B≤ibT C。结合关于可计算偏移的已知性质,我们便可得到上述主要定理。     

永真假性的研究

我们假定读者已经知道一个狭义谓词演算公式α(其中可出现“等号”,下同)的永真性和可满足性的定义及其一些最简单的性质。不可满足的公式亦叫做永假公式。所谓永真假性问题是:     

萨奎斯特逻辑的格

以萨奎斯特公式为额外公理添加到极小正规逻辑K上得到的逻辑都是完全的。这样得到的逻辑被称为萨奎斯特逻辑。所有的萨奎斯特逻辑组成了一个格。这个格中有可数无穷长的链以及可数无穷长的反链,格中的每个逻辑相对于格的不完全度是1。另外,萨奎斯特逻辑格的子格E具有规整的结构。     

可数图灵理想的恰对和一致上界

一个（图灵）理想,是满足两个封闭条件的图灵度集合：向下封闭;任意,中一对图灵度的上确界也在,中。可数理想不仅在图灵度整体性质的研究中有着重要意义,而且在对哥德尔可构成集合L精细结构的早期研究中也发挥过重要作用。研究可数理想的两个重要概念是：恰对和一致上界。借助这两个概念,我们可以将可数理想简化为一个（一致上界）或者一对（恰对）图灵度。通过前人的研究,我们可以发现这两个概念是紧密相连的,同时我们也可以对它们的关系提出进一步的问题。在本文中,我们证明以下定理：任给一个可数理想I,都存在两个I的一致上界a0和a1,同时a0和a1构成,的一个恰对。此定理从正面回答了Lerman提出的关于算术图灵度构成的理想的一个问题。此定理的证明实际上是经过小心修改的、典型的恰对构造。我们在典型恰对构造的过程中,加入一些微妙的限制,使得形成恰对的两个图灵度a0和a1可以各自独立地在一定程度上用逼近的办法还原整个构造,从而分别给出可数理想I的一致枚举。在a0和a1分别的逼近中,我们引入了有穷损坏方法。本文的最后指出a0和a1的图灵跃迁的一些性质。     

LR度中完备链的存在性(英文)

我们证明存在一个完备实数集使得在这个完备集中任何两个实数都是LR可比较的。"在LR度中是否每个完备集都包含一个不可数的反链?"这一问题多次被提及。显然,图灵归约蕴含LR归约。但过去十年的研究表明,两者之间还是存在着显著的差异的。那么一个很自然的疑问就是,图灵度中的基本结论——每个完备集都包含两个图灵不可比实数——是否在LR度中仍为真。     

让小我融入大我:适恰自尊的积极心理学意义

本研究基于本土自尊理论,将建立在适度恰当满足大小我需要基础上的自尊称为“适恰自尊”,并从个体,人际与集体三个层面揭示其积极心理学意义。结果发现：（1）在个体层面,适恰自尊与青少年主观幸福感显著正相关;（2）在人际层面,适恰自尊会放大来自他人（即父母）适恰自尊对青少年主观幸福感的积极影响;（3）在集体层面,大学新生的适恰自尊与大我自尊显著正相关,并有利于大学新生在入学一年内通过逐步建立大我自尊和小我自尊满足多重基本心理需要。本研究通过揭示中国人理想型自尊的内涵和机制,将会助力中国人理性平和,积极向上社会心态的建立与提升。     

所有非Z_类的类的悖论

令Z为一个满足下列两条件的性质: (1) x(x∈x→Z(x)); (2) x(Z(x)→y∈x.Z(y))。称具有性质Z的类为Z_类。令K_Z是由所有非Z_类组成的类,即,K_Z={x|～Z(x)}。     

NExt（S4）中Bull逻辑再探

本文重新考察Bull在1964给出的一个结论：以纯句法方式定义的一些扩张S4的正规模态逻辑具有有穷模型性质。本文修订Bull的代数证明。对于新定义的S4的Bull公式,证明通过它们在S4基础上生成的正规模态逻辑都具有有穷模型性质。这是关于模态逻辑的有穷模型性质的句法结论。本文还证明,相对于所有克里普克框架类而言,并非所有S4的Bull公式都具有一阶对应句子。     

Computing finite models by reduction to function-free clause logic

Recent years have seen considerable interest in procedures for computing finite models of first-order logic specifications. One of the major paradigms, MACE-style model building, is based on reducing model search to a sequence of propositional satisfiability problems and applying (efficient) SAT solvers to them. A problem with this method is that it does not scale well because the propositional formulas to be considered may become very large.We propose instead to reduce model search to a sequence of satisfiability problems consisting of function-free first-order clause sets, and to apply (efficient) theorem provers capable of deciding such problems. The main appeal of this method is that first-order clause sets grow more slowly than their propositional counterparts, thus allowing for more space efficient reasoning.In this paper we describe our proposed reduction in detail and discuss how it is integrated into the Darwin prover, our implementation of the Model Evolution calculus. The results are general, however, as our approach can be used in principle with any system that decides the satisfiability of function-free first-order clause sets.To demonstrate its practical feasibility, we tested our approach on all satisfiable problems from the TPTP library. Our methods can solve a significant subset of these problems, which overlaps but is not included in the subset of problems solvable by state-of-the-art finite model builders such as Paradox and Mace4.     

Perfect validity,entailment and paraconsistency

This paper treats entailment as a subrelation of classical consequence and deducibility. Working with a Gentzen set-sequent system, we define an entailment as a substitution instance of a valid sequent all of whose premisses and conclusions are necessary for its classical validity. We also define a sequent Proof as one in which there are no applications of cut or dilution. The main result is that the entailments are exactly the Provable sequents. There are several important corollaries. Every unsatisfiable set is Provably inconsistent. Every logical consequence of a satisfiable set is Provable therefrom. Thus our system is adequate for ordinary mathematical practice. Moreover, transitivity of Proof fails upon accumulation of Proofs only when the newly combined premisses are inconsistent anyway, or the conclusion is a logical truth. In either case Proofs that show this can be effectively determined from the Proofs given. Thus transitivity fails where it least matters — arguably, where it ought to fail! We show also that entailments hold by virtue of logical form insufficient either to render the premisses inconsistent or to render the conclusion logically true. The Lewis paradoxes are not Provable. Our system is distinct from Anderson and Belnap's system of first degree entailments, and Johansson's minimal logic. Although the Curry set paradox is still Provable within naive set theory, our system offers the prospect of a more sensitive paraconsistent reconstruction of mathematics. It may also find applications within the logic of knowledge and belief.     

Parallel structure: A source of facilitation in sentence comprehension

Reading time for the second clause of a conjoined sentence was found to be faster when the clause was structurally similar to the first clause than when the clausal structures differed. This “parallel structure” effect was found for each of several types of structures, including active versus passive constructions, direct object versus sentential complement (minimal vs. nonminimal attachment), nonshifted versus shifted heavy noun phrase, agent versus theme, and animate versus inanimate noun phrase. The pervasiveness of the effect ruled out some hypotheses about its basis, including the hypothesis that it would occur only when a subject’s just having processed a structure would affect how temporary ambiguities are resolved. Detailed analysis of the data suggested the existence of several distinct sources of the effect and provided indirect evidence that people typically compute both a surface structure and an S-structure representation of a sentence.     

On Consistent Subsets of Large Sets of Satisfiable Sentences

We extend some results of Adam Kolany to show that large sets of satisfiable sentences generally contain equally large subsets of mutually consistent sentences. In particular, this is always true for sets of uncountable cofinality, and remains true for sets of denumerable cofinality if we put appropriate bounding conditions on the sentences. The results apply to both the propositional and the predicate calculus. To obtain these results, we use delta sets for regular cardinals, and, for singular cardinals, a generalization of delta sets. All of our results are theorems in ZFC.     

A Note on the Conversion of Item Parameters Standard Errors

The relations among alternative parameterizations of the binary factor analysis (FA) model and two-parameter logistic (2PL) item response theory (IRT) model have been thoroughly discussed in literature. However, the conversion formulas widely available are mainly for transforming parameter estimates from one parameterization to another. There is a lack of discussion about the standard error (SE) conversion among different parameterizations, when SEs of IRT model parameters are often of immediate interest to practitioners. This article provides general formulas for computing the SEs of transformed parameter values, when these parameters are transformed from FA to IRT models. These formulas are suitable for unidimensional 2PL, multidimensional 2PL, and bi-factor 2PL models. A simulation study is conducted to verify the formula by providing empirical evidence. A real data example is given in the end for an illustration.     

Processing relative clauses in Chinese

This paper reports results from a self-paced reading study in Chinese that demonstrates that object-extracted relative clause structures are less complex than corresponding subject-extracted structures. These results contrast with results from processing other Subject-Verb-Object languages like English, in which object-extracted structures are more complex than subject-extracted structures. A key word-order difference between Chinese and other Subject-Verb-Object languages is that Chinese relative clauses precede their head nouns. Because of this word order difference, the results follow from a resource-based theory of sentence complexity, according to which there is a storage cost associated with predicting syntactic heads in order to form a grammatical sentence. The results are also consistent with a theory according to which people have less difficulty processing embedded clauses whose word order matches the word order in main clauses. Some corpus analyses of Chinese texts provide results that constrain the classes of possible frequency-based theories. Critically, these results demonstrate that there is nothing intrinsically easy about extracting from subject position: depending on the word order in the main clause and in a relative clause, extraction from object position can be easier to process in some circumstances.     

Syntactic analysis in sentence comprehension: Effects of dependency types and grammatical constraints

This paper presents three experiments on the parsing of Italian wh-questions that manipulate the wh-type (whovs. which-N)and the whextraction site (main clause, dependent clause with or without complementizer). The aim of these manipulations is to see whether the parser is sensitive to the type of dependencies being processed and whether the processing effects can be explained by a unique processing principle, the minimal chain principle (MCP; De Vincenzi, 1991). The results show that the parser, following the MCP, prefers structures with fewer and less complex chains. In particular: (1) There is a processing advantage for the wh-subject extractions, the structures with less complex chains; (2) there is a processing dissociation between the whoand which questions; (3) the parser respects the principle that governs the well-formedness of the empty categories (ECP).     

A generalized expression for the reliability of measures

In certain situations it is important to obtain as many measures as possible, all presumably measuring the same function, for each of a group of persons. In general the number and source of the measures may vary from one member of the group to another. We take the mean of the measures for each person as the best estimate of the function for that person. The conventional formulas can not be used to determine the reliability of a set of means so obtained. A formula is developed which provides a unique estimate of the reliability of such a set of means. The formula is more general than some of the well-known reliability formulas, so that these formulas are shown to be special cases of the more general formula.     

Paraconsistency in classical logic

Classical propositional logic can be characterized, indirectly, by means of a complementary formal system whose theorems are exactly those formulas that are not classical tautologies, i.e., contradictions and truth-functional contingencies. Since a formula is contingent if and only if its negation is also contingent, the system in question is paraconsistent. Hence classical propositional logic itself admits of a paraconsistent characterization, albeit “in the negative”. More generally, any decidable logic with a syntactically incomplete proof theory allows for a paraconsistent characterization of its set of theorems. This, we note, has important bearing on the very nature of paraconsistency as standardly characterized.