共查询到20条相似文献,搜索用时 31 毫秒
1.
2.
If all dependent expressions were adjacent some variety of immediate constituent analysis would suffice for grammar, but syntactic
and semantic mismatches are characteristic of natural language; indeed this is a, or the, central problem in grammar. Logical
categorial grammar reduces grammar to logic: an expression is well-formed if and only if an associated sequent is a theorem
of a categorial logic. The paradigmatic categorial logic is the Lambek calculus, but being a logic of concatenation the Lambek
calculus can only capture discontinuous dependencies when they are peripheral. In this paper we present the displacement calculus,
which is a logic of intercalation as well as concatenation and which subsumes the Lambek calculus. On the empirical side,
we apply the new calculus to discontinuous idioms, quantification, VP ellipsis, medial extraction, pied-piping, appositive
relativisation, parentheticals, gapping, comparative subdeletion, cross-serial dependencies, reflexivization, anaphora, dative
alternation, and particle shift. On the technical side, we prove that the calculus enjoys Cut-elimination. 相似文献
3.
The language of signed formulas offers a first-order classical logic framework for automated reasoning in multiple-valued logics. It is sufficiently general to include both annotated logics and fuzzy operator logics. Signed resolution unifies the two inference rules of annotated logics, thus enabling the development of an SLD-style proof procedure for annotated logic programs. Signed resolution also captures fuzzy resolution. The logic of signed formulas offers a means of adapting most classical inference techniques to multiple-valued logics. 相似文献
4.
Deepak D’Souza Pavithra Prabhakar 《International Journal on Software Tools for Technology Transfer (STTT)》2007,9(1):1-4
We show that the pointwise version of the logic MTL is strictly less expressive than the continuous version, over finitewords. The proof is constructive in that we exhibit a timed language, which is definable in the continuous semantics but is
not definable in the pointwise semantics. 相似文献
5.
Although a large number of formal methods have been reported in the literature, most of them are applicable only at the initial stages of software development. A major reason for this situation is that those formalisms lack expressiveness to describe the behavior of systems with respect to their underlying configurations. On the other hand, recent experience has shown that the complex nature of distributed systems is conveniently described, constructed and managed in terms of their configuration. In this context, with the twin objectives of accurately modelling the real-timed behavior of distributed systems and supporting the analysis of timing behavior with respect to their underlying configurations, we formulate a logic language called distributed logic (DL). DL is a first-order logic augmented with temporal and spatial modalities. The semantics of DL are based on ideas drawn from both the interleaving and partial order models. In addition to the syntax and semantics of the logic, a formal proof scheme for a distributed programming model is also presented. Finally, use of the proof method is illustrated through the analysis of the real-time properties of a sample problem. 相似文献
6.
The safe belief semantics uses intermediate logics to definean extension of answer sets to all propositional formulas, butonly considering one kind of negation. In this work we extendsafe beliefs adding the strong negation connective. The mainfeature of our extension is that strong negation can occur beforeany formula, and not only at the atomic level. We give resultsconcerning the relation between strong negation extensions ofintermediate logics and safe beliefs and consider the way inwhich strong negation can be eliminated from any formula whilepreserving its semantics. We also propose two new notions ofequivalence: substitution equivalence and contextualized equivalence.We prove that they are both more general than strong equivalenceand, for propositional formulas where strong negation may occurat the non-atomic level, substitution equivalence captures anotion of equivalence that cannot be captured by strong equivalencealone. 相似文献
7.
From an arbitrary temporal logic institution we show how to set up the corresponding institution of objects. The main properties
of the resulting institution are studied and used in establishing a categorial, denotational semantics of several basic constructs
of object specification, namely aggregation (parallel composition), interconnection, abstraction (interfacing) and monotonic
specialization. A duality is established between the category of theories and the category of objects, as a corollary of the
Galois correspondence between these concrete categories. The special case of linear temporal logic is analysed in detail in
order to show that categorial products do reflect interleaving and reducts may lead to internal non-determinism.
Received: 30 May 1996 / 4 November 1997 相似文献
8.
Model checking of asynchronous systems is traditionally based on the interleaving model, where an execution is modeled by a total order between atomic events. Recently, the use of partial order semantics, representing the causal order between events, is becoming popular. This paper considers the model checking problem for partial-order temporal logics. Solutions to this problem exist for partial order logics over local states. For the more general global logics that are interpreted over global states, only undecidability results have been proved. In this paper, we present a decision procedure for a partial order temporal logic over global states. We also sharpen the undecidability results by showing that a single until operator is sufficient for undecidability.A preliminary version of this paper appears in Proceedings of the 25th International Colloquium on Automata, Languages, and Programming (ICALP98), LNCS 1443, pp. 41–52, 1998. 相似文献
9.
The complexity of LTrL, a global linear time temporal logic over traces is investigated. The logic is global because the truth of a formula is evaluated in a global state, also called configuration. The logic is shown to be non-elementary with the main reason for this complexity being the nesting of until operators in formulas. The fragment of the logic without the until operator is shown to be EXPSPACE-hard.Supported by Polish KBN grant No. 8 T11C 002 11. 相似文献
10.
Hans de Nivelle 《Journal of Automated Reasoning》2011,47(4):399-425
We introduce a semantics for classical logic with partial functions, in which ill-typed formulas are guaranteed to have no
truth value, so that they cannot be used in any form of reasoning. The semantics makes it possible to mix reasoning about
types and preconditions with reasoning about other properties. This makes it possible to deal with partial functions with
preconditions of unlimited complexity. We show that, in spite of its increased complexity, the semantics is still a natural
generalization of first-order logic with simple types. If one does not use the increased expressivity, the type system is
not stronger than classical logic with simple types. We will define two sequent calculi for our semantics, and prove that
they are sound and complete. The first calculus follows the semantics closely, and hence its completeness proof is fairly
straightforward. The second calculus is further away from the semantics, but more suitable for practical use because it has
better proof theoretic properties. Its completeness can be shown by proving that proofs from the first calculus can be translated. 相似文献
11.
12.
13.
We consider the non-orthodox proof rules of hybrid logic from the viewpoint of topological semantics. Topological semantics is more general than Kripke semantics. We show that the hybrid proof rule BG is topologically not sound. Indeed, among all topological spaces the BG rule characterizes those that can be represented as a Kripke frame (i.e., the Alexandroff spaces). We also demonstrate that, when the BG rule is dropped and only the Name rule is kept, one can prove a general topological completeness result for hybrid logics axiomatized by pure formulas. Finally, we indicate some limitations of the topological expressive power of pure formulas. All results generalize to neighborhood frames. 相似文献
14.
A LOGIC OF ARGUMENTATION FOR REASONING UNDER UNCERTAINTY 总被引:5,自引:0,他引:5
Paul Krause Simon Ambler Morten Elvang-Goransson John Fox 《Computational Intelligence》1995,11(1):113-131
We present the syntax and proof theory of a logic of argumentation, LA. We also outline the development of a category theoretic semantics for LA. LA is the core of a proof theoretic model for reasoning under uncertainty. In this logic, propositions are labeled with a representation of the arguments which support their validity. Arguments may then be aggregated to collect more information about the potential validity of the propositions of interest. We make the notion of aggregation primitive to the logic, and then define strength mappings from sets of arguments to one of a number of possible dictionaries. This provides a uniform framework which incorporates a number of numerical and symbolic techniques for assigning subjective confidences to propositions on the basis of their supporting arguments. These aggregation techniques are also described with examples. 相似文献
15.
A resolution based proof system for a Temporal Logic of Possible Belief is presented. This logic is the combination of the branching-time temporal logic CTL (representing change over time) with the modal logic KD45 (representing belief ). Such combinations of temporal or dynamic logics and modal logics are useful for specifying complex properties of multi-agent systems. Proof methods are important for developing verification techniques for these complex multi-modal logics. Soundness, completeness and termination of the proof method are shown and simple examples illustrating its use are given. 相似文献
16.
17.
描述逻辑(DL)一族知识表示形式系统,是人工智能领域的一个热门研究方向。循环定义下描述逻辑系统的表达在许多情况下更符合人们的直觉,而且具有更强的表达力,是非循环定义下的描述逻辑系统不可代替的。首先给出描述逻辑系统FLε有最大不动点模型的证明,然后初步探讨基于最大不动点语义下描述逻辑系统FLε循环定义的包含关系推理算法,并给出算法的可靠性和完全性证明。 相似文献
18.
Mary Dalrymple John Lamping Fernando Pereira Vijay Saraswat 《Journal of Logic, Language and Information》1997,6(3):219-273
The relationship between Lexical-Functional Grammar (LFG) functional structures (f-structures) for sentences and their semanticinterpretations can be formalized in linear logic in a way thatcorrectly explains the observed interactions between quantifier scopeambiguity, bound anaphora and intensionality.Our linear-logic formalization of the compositional properties ofquantifying expressions in natural language obviates the need forspecial mechanisms, such as Cooper storage, in representing thescoping possibilities of quantifying expressions. Instead, thesemantic contribution of a quantifier is recorded as a linear-logicformula whose use in a proof will establish the scope of thequantifier. Different proofs can lead to different scopes. In eachcomplete proof, the properties of linear logic ensure thatquantifiers are properly scoped.The interactions between quantified NPs and intensional verbs such asseek are also accounted for in this deductive setting. A singlespecification in linear logic of the argument requirements ofintensional verbs is sufficient to derive the correct readingpredictions for intensional-verb clauses both with nonquantified andwith quantified direct objects. In particular, both de dictoand de re readings are derived for quantified objects. Theeffects of type-raising or quantifying-in rules in other frameworksjust follow here as linear-logic theorems.While our approach resembles current categorial approaches inimportant ways (Moortgat, 1988, 1992a; Carpenter, 1993; Morrill, 1994)it differs from them in allowing the greater compositional flexibility ofcategorial semantics (van Benthem, 1991)while maintaining a precise connection to syntax. As a result, we areable to provide derivations for certain readings of sentences withintensional verbs and complex direct objects whose derivation inpurely categorial accounts of the syntax-semantics interface appearsto require otherwise unnecessary semantic decompositions of lexicalentries. 相似文献
19.
This paper presents some techniques which bound the proof search space in propositional intuitionistic logic. These techniques are justified by Kripke semantics and are the backbone of a tableau based theorem prover (PITP) implemented in C++. PITP and some known theorem provers are compared using the formulas of ILTP benchmark library. It turns out that PITP is, at the moment, the propositional prover that solves most formulas of the library. 相似文献
20.
《Theoretical computer science》1996,165(1):171-200
In this paper, we propose a three-valued completion semantics for abductive logic programs, which solves some problems associated with the Console et al. two-valued completion semantics. The semantics is a generalization of Kunen's completion semantics for general logic programs, which is known to correspond very well to a class of effective proof procedures for general logic programs. Secondly, we propose a proof procedure for abductive logic programs, which is a generalization of a proof procedure for general logic programs based on constructive negation. This proof procedure is sound and complete with respect to the proposed semantics. By generalizing a number of results on general logic programs to the class of abductive logic programs, we present further evidence for the idea that limited forms of abduction can be added quite naturally to general logic programs. 相似文献