An Event-Based Fragment of First-Order Logic over Intervals

We consider a new fragment of first-order logic with two variables. This logic is defined over interval structures. It constitutes unary predicates, a binary predicate and a function symbol. Considering such a fragment of first-order logic is motivated by defining a general framework for event-based interval temporal logics. In this paper, we present a sound, complete and terminating decision procedure for this logic. We show that the logic is decidable, and provide a NEXPTIME complexity bound for satisfiability. This result shows that even a simple decidable fragment of first-order logic has NEXPTIME complexity.     

Determinization of Transducers over Infinite Words: The General Case

We consider transducers over infinite words with a Büchi or a Muller acceptance condition. We give characterizations of functions that can be realized by Büchi and Muller sequential transducers. We describe an algorithm to determinize transducers defining functions over infinite words.     

Relating Z and First-Order Logic

Despite being widely regarded as a gloss on first-order logic and set theory, Z has not been found to be very supportive of proof. This paper attempts to distinguish between the different philosophies of proof in Z. It discusses some of the issues which must be addressed in creating a proof technology for Z, namely schemas, undefinedness, and what kind of logic to use. Received February 2000 / Accepted in revised form April 2000     

Adding For-Loops to First-Order Logic

We study the query language BQL: the extension of the relational algebra with for-loops. We also study FO(FOR): the extension of first-order logic with a for-loop variant of the partial fixpoint operator. In contrast to the known situation with query languages, which include while-loops instead of for-loops, BQL and FO(FOR) are not equivalent. Among the topics we investigate are: the precise relationship between BQL and FO(FOR); inflationary versus noninflationary iteration; the relationship with logics that have the ability to count; and nested versus unnested loops.     

Infinite Spectra of First-Order Properties for Random Hypergraphs

We study the asymptotic behavior of probabilities of first-order properties for random uniform hypergraphs. In 1990, J. Spencer introduced the notion of a spectrum for graph properties and proved the existence of a first-order property with an infinite spectrum. In this paper we give a definition of a spectrum for properties of uniform hypergraphs and establish an almost tight bound for the minimum quantifier depth of a first-order formula with infinite spectrum.     

First-Order Logic with Two Variables and Unary Temporal Logic

We investigate the power of first-order logic with only two variables over ω-words and finite words, a logic denoted by FO². We prove that FO² can express precisely the same properties as linear temporal logic with only the unary temporal operators: “next,” “previously,” “sometime in the future,” and “sometime in the past,” a logic we denote by unary-TL Moreover, our translation from FO² to unary-TL converts every FO² formula to an equivalent unary-TL formula that is at most exponentially larger and whose operator depth is at most twice the quantifier depth of the first-order formula. We show that this translation is essentially optimal. While satisfiability for full linear temporal logic, as well as for unary-TL, is known to be PSPACE-complete, we prove that satisfiability for FO² is NEXP-complete, in sharp contrast to the fact that satisfiability for FO³ has nonelementary computational complexity. Our NEXP upper bound for FO² satisfiability has the advantage of being in terms of the quantifier depth of the input formula. It is obtained using a small model property for FO² of independent interest, namely, a satisfiable FO² formula has a model whose size is at most exponential in the quantifier depth of the formula. Using our translation from FO² to unary-TL we derive this small model property from a corresponding small model property for unary-TL. Our proof of the small model property for unary-TL is based on an analysis of unary-TL types.     

Quantifier Alternation in First-Order Formulas with Infinite Spectra

The spectrum of a first-order formula is the set of numbers α such that for a random graph in a binomial model where the edge probability is a power function of the number of graph vertices with exponent ?α the truth probability of this formula does not tend to either zero or one. In 1990 J. Spenser proved that there exists a first-order formula with an infinite spectrum. We have proved that the minimum quantifier depth of a first-order formula with an infinite spectrum is either 4 or 5. In the present paper we find a wide class of first-order formulas of depth 4 with finite spectra and also prove that the minimum quantifier alternation number for a first-order formula with an infinite spectrum is 3.     

Natural Deduction for First-Order Hybrid Logic

This is a companion paper to Braüner (2004b, Journal of Logic and Computation 14, 329–353) where a natural deduction system for propositional hybrid logic is given. In the present paper we generalize the system to the first-order case. Our natural deduction system for first-order hybrid logic can be extended with additional inference rules corresponding to conditions on the accessibility relations and the quantifier domains expressed by so-called geometric theories. We prove soundness and completeness and we prove a normalisation theorem. Moreover, we give an axiom system first-order hybrid logic.     

Reasoning About Truth in First-Order Logic

First, we describe a psychological experiment in which the participants were asked to determine whether sentences of first-order logic were true or false in finite graphs. Second, we define two proof systems for reasoning about truth and falsity in first-order logic. These proof systems feature explicit models of cognitive resources such as declarative memory, procedural memory, working memory, and sensory memory. Third, we describe a computer program that is used to find the smallest proofs in the aforementioned proof systems when capacity limits are put on the cognitive resources. Finally, we investigate the correlation between a number of mathematical complexity measures defined on graphs and sentences and some psychological complexity measures that were recorded in the experiment.     

On First-Order Logic and CPDA Graphs

Higher-order pushdown automata (n-PDA) are abstract machines equipped with a nested ‘stack of stacks of stacks’. Collapsible pushdown automata (n-CPDA) extend these devices by adding ‘links’ to the stack and are equi-expressive for tree generation with simply typed λY terms. Whilst the configuration graphs of HOPDA are well understood, relatively little is known about the CPDA graphs. The order-2 CPDA graphs already have undecidable MSO theories but it was only recently shown by Kartzow (Log. Methods Comput. Sci. 9(1), 2013) that first-order logic is decidable at the second level. In this paper we show the surprising result that first-order logic ceases to be decidable at order-3 and above. We delimit the fragments of the decision problem to which our undecidability result applies in terms of quantifer alternation and the orders of CPDA links used. Additionally we exhibit a natural sub-hierarchy enjoying limited decidability.     

命题逻辑提升到一阶逻辑上的子句消去方法

在基于命题逻辑的可满足性问题（SAT）求解器和基于一阶逻辑的定理证明器上，子句集简化一直是必不可少的步骤，而其中子句消去方法在这些子句集简化方法中是非常重要的组成部分。将命题逻辑中的子句消去方法归结隐藏恒真消去方法（RHTE）和归结隐藏包含消去方法（RHSE）提升到一阶逻辑上，并且利用蕴含模归结原则（IMR）证明了这种提升方式在一阶逻辑上具有可靠性（Soundness），即依据这两种子句消去方法删除一阶逻辑公式集中的子句，并不会改变公式集的可满足性或者不可满足性。此外，将这两个方法与一阶逻辑子句消去方法锁子句消去方法（BCE）和归结包含消去方法（RSE）进行组合推广，发展得到一阶逻辑上新型子句消去方法（BC+RHS）E、（RS+RHT）E和（RHS+RHT）E，并且证明了这3种子句消去方法在一阶逻辑上的可靠性。最后，分析比较了这些子句消去方法的有效性，并且证明了这3种新型子句消去方法比组成它们的原始子句消去方法均具有更高的有效性。     

基于一阶模态逻辑的模糊推理

研究基于可信度的模糊一阶模态逻辑,给出了基于常域的模糊一阶模态逻辑语义以及推理形式系统描述.为有效进行模糊断言间的推理,考虑了模糊约束的概念.模糊约束是一个表达式,其中既有语法成分又包含意义信息.模糊推理形式系统中的基本对象是模糊约束,针对模糊约束引进可满足性概念,研究模糊约束可满足性相关性质.利用模糊约束的概念,模糊断言间的推理可以直接在语义环境下加以考虑,因此,以模糊约束为基本元素的模糊推理形式系统随之建立.主要分析新产生断言有效性与模糊约束集可满足性之间的关系,并在此基础上给出了模糊推理形式系统的推理规则.进一步的工作可探讨模糊推理形式系统的可靠性与完全性,建立推理过程的能行机制.研究结果可在人工智能和计算机科学等领域得以应用.     

Weak Abelian Periodicity of Infinite Words

An infinite word is called weak abelian periodic if it can be represented as an infinite concatenation of finite words with identical frequencies of letters. In the paper we undertake a general study of the weak abelian periodicity property. We consider its relation with the notions of balance and letter frequency, and study operations preserving weak abelian periodicity. We establish necessary and sufficient conditions for the weak abelian periodicity of fixed points of uniform binary morphisms. Finally, we discuss weak abelian periodicity in minimal subshifts.     

Formalization of the Resolution Calculus for First-Order Logic

I present a formalization in Isabelle/HOL of the resolution calculus for first-order logic with formal soundness and completeness proofs. To prove the calculus sound, I use the substitution lemma, and to prove it complete, I use Herbrand interpretations and semantic trees. The correspondence between unsatisfiable sets of clauses and finite semantic trees is formalized in Herbrand’s theorem. I discuss the difficulties that I had formalizing proofs of the lifting lemma found in the literature, and I formalize a correct proof. The completeness proof is by induction on the size of a finite semantic tree. Throughout the paper I emphasize details that are often glossed over in paper proofs. I give a thorough overview of formalizations of first-order logic found in the literature. The formalization of resolution is part of the IsaFoL project, which is an effort to formalize logics in Isabelle/HOL.     

An Algorithm for Dual Transformation in First-Order Logic

The transformation between conjunctive and disjunctive canonical forms is useful in domains such as theorem proving, function minimization, and knowledge representation. In this paper, we present a concurrent algorithm for this transformation, suitable for first-order logic theories. The proposed algorithm use the holographic relation between these normal forms in order to avoid the generation of noncondensed and subsumed (dual) clauses. We also stress the facts that, in first-order logic, this transformation is asymmetric and that disjunctive normal form, in some special cases, may be not unique, depending on choices about which subsumptions are allowed or not. The algorithm, which is part of a theorem-proving knowledge representation project, has been implemented and tested.     

Toward Effective Knowledge Acquisition with First-Order Logic Induction

Knowledge acquisition with machine learning techniques is a fundamental requirement for knowledge discovery from databases and data mining systems.Two techniques in particular-inductive learning and theory revision-have been used toward this end.A method that combines both approaches to effectively acquire theories (regularity) from a set of training examples is presented.Inductive learning is used to acquire new regularity from the training examples;and theory revision is used to improve an initial theory.In addition,a theory preference criterion that is a combination of the MDL-based heuristic and the Laplace estimate has been successfully employed in the selection of the promising theory.The resulting algorithm developed by integrating inductive learning and theory revision and using the criterion has the ability to deal with complex problems,obtaining useful theories in terms of its predictive accuracy.     

语义网的一阶逻辑推理技术支持

研究了一阶逻辑推理工具对语义网的推理支持.语义网的关键推理问题可以化为公式的可满足性判定问题.一阶逻辑的自动定理证明器可以证明不可满足性,而有限模型查找器为可满足的公式在有限域内构造模型.提出在语义网的推理中,同时使用定理证明器和有限模型查找器.实验结果表明,这样可以解决描述逻辑工具的不足,并可以弥补定理证明器对可满足的公式推理的不完备性.     

Partial Instantiation Methods for Inference in First-Order Logic

Satisfiability algorithms for propositional logic have improved enormously in recently years. This improvement increases the attractiveness of satisfiability methods for first-order logic that reduce the problem to a series of ground-level satisfiability problems. R. Jeroslow introduced a partial instantiation method of this kind that differs radically from the standard resolution-based methods. This paper lays the theoretical groundwork for an extension of his method that is general enough and efficient enough for general logic programming with indefinite clauses. In particular we improve Jeroslow's approach by (1) extending it to logic with functions, (2) accelerating it through the use of satisfiers, as introduced by Gallo and Rago, and (3) simplifying it to obtain further speedup. We provide a similar development for a dual partial instantiation approach defined by Hooker and suggest a primal–dual strategy. We prove correctness of the primal and dual algorithms for full first-order logic with functions, as well as termination on unsatisfiable formulas. We also report some preliminary computational results.     

基于一阶逻辑的RDF模型的研究

XML为互联网应用提供了语法互操作性统一标准,而资源描述框架RDF定义了支持语义互操作的框架模型。作为RDF数据模型的类型系统,资源描述框架模式RDFS定义了一套扩充新的建模原语及其语义约束的机制。由于整个互联网语义化过程都以RDF模型为底层的模型支持,RDF数据模型及其类型系统的形式化程度直接影响和制约着更高层次上的语言和模型的形式化能力和推理能力。文章首先对RDFS类型系统做了非形式化分析,然后基于一阶逻辑定义了一套RDFS类型系统中对应类层次模型、类-实例模型和核心概念约束模型的事实-规则集。