ALBERT

All Library Books, journals and Electronic Records Telegrafenberg

Your email was sent successfully. Check your inbox.

An error occurred while sending the email. Please try again.

Proceed reservation?

Export
Filter
  • Articles  (2,229)
  • Oxford University Press  (2,229)
  • Journal of Logic and Computation  (355)
  • 3629
  • Mathematics  (2,229)
  • Law
Collection
  • Articles  (2,229)
Publisher
  • Oxford University Press  (2,229)
Years
Topic
  • 1
    Publication Date: 2015-09-29
    Description: Unification grammars (UGs) are a grammatical formalism that underlies several contemporary linguistic theories, including lexical-functional grammar and head-driven phrase-structure grammar. UG is an especially attractive formalism because of its expressivity, which facilitates the expression of complex linguistic structures and relations. Formally, UG is Turing-complete, generating the entire class of recursively enumerable languages. This expressivity, however, comes at a price: the universal recognition problem is undecidable for arbitrary unification grammars. We define a constrained version of UG that is equivalent to range concatenation grammar, a formalism that generates exactly the class of languages recognizable in deterministic polynomial time. We thus obtain a constrained unification grammar formalism that guarantees efficient processing.
    Print ISSN: 0955-792X
    Electronic ISSN: 1465-363X
    Topics: Computer Science , Mathematics
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 2
    Publication Date: 2015-09-29
    Description: The syntactic concept lattice is a residuated lattice associated with a given formal language; it arises naturally as a generalization of the syntactic monoid in the analysis of the distributional structure of the language. In this article we define the syntactic concept lattice and present its basic properties, and its relationship to the universal automaton and the syntactic congruence; we consider several different equivalent definitions, as Galois connections, as maximal factorizations and finally using universal algebra to define it as an object that has a certain universal (terminal) property in the category of complete idempotent semirings that recognize a given language, applying techniques from automata theory to the theory of context-free grammars (CFGs). We conclude that grammars that are minimal, in a certain weak sense, will always have non-terminals that correspond to elements of this lattice, and claim that the syntactic concept lattice provides a natural system of categories for representing the denotations of CFGs.
    Print ISSN: 0955-792X
    Electronic ISSN: 1465-363X
    Topics: Computer Science , Mathematics
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 3
    Publication Date: 2015-09-29
    Description: In this article we offer a formal account of reasoning with legal cases in terms of argumentation schemes. These schemes, and undercutting attacks associated with them, are formalized as defeasible rules of inference within the ASPIC+ framework. We begin by modelling the style of reasoning with cases developed by Aleven and Ashley in the CATO project, which describes cases using factors, and then extend the account to accommodate the dimensions used in Rissland and Ashley's earlier HYPO project. Some additional scope for argumentation is then identified and formalized.
    Print ISSN: 0955-792X
    Electronic ISSN: 1465-363X
    Topics: Computer Science , Mathematics
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 4
    Publication Date: 2015-09-29
    Description: The aim of this article is to provide a metalogical systematization in the area of deontic action logic based on Boolean algebra. Differences among the systems involve two aspects: the level of closedness of a deontic action logic and the possibility of performing no action at all . It is also shown that the existing definitions of obligation in these systems are unacceptable due to their non-intuitive interpretation or paradoxical consequences. As a solution we propose a minimal axiomatic characterization of obligation with an adequate class of models. This article also describes how deontic action logic can be used to answer the questions from the Polish driving license test.
    Print ISSN: 0955-792X
    Electronic ISSN: 1465-363X
    Topics: Computer Science , Mathematics
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 5
    Publication Date: 2015-09-29
    Description: We investigate properties of the formula p -〉 p in the basic modal logic K . We show that K satisfies an infinitary weaker variant of the rule of margins -〉 / , ¬ , and as a consequence, we obtain various negative results about admissibility and unification in K . We describe a complete set of unifiers (i.e. substitutions making the formula provable) of p -〉 p , and use it to establish that K has the worst possible unification type: nullary. In well-behaved transitive modal logics, admissibility and unification can be analysed in terms of projective formulas, introduced by Ghilardi; in particular, projective formulas coincide for these logics with formulas that are admissibly saturated (i.e. derive all their multiple-conclusion admissible consequences) or exact (i.e. axiomatize a theory of a substitution). In contrast, we show that in K , the formula p -〉 p is admissibly saturated, but neither projective nor exact. All our results for K also apply to the basic description logic $$\mathcal{ALC}$$ .
    Print ISSN: 0955-792X
    Electronic ISSN: 1465-363X
    Topics: Computer Science , Mathematics
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 6
    Publication Date: 2015-05-29
    Description: We introduce a new belief revision operator called evaluative multiple revision. Belief states in the revision are belief bases with core beliefs. New information that triggers the revision is evaluated beliefs, some of which are evaluated by the core beliefs as plausible and the others implausible. We characterize this operator by axiomatic postulates in the AGM (named after the three authors, i. e. C.E. Alchourrón, P. Gärdenfors, and D. Makinson, in literature of belief revision) style. Two functional constructions are given for the operator based on evaluative kernel sets and evaluative remainder sets, respectively, with representation theorems proved. We also compare some related works with ours and show the generality of the operator.
    Print ISSN: 0955-792X
    Electronic ISSN: 1465-363X
    Topics: Computer Science , Mathematics
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 7
    Publication Date: 2015-05-29
    Description: Logic-based abduction is an important reasoning method with many applications in Artificial Intelligence including diagnosis, planning, and configuration. The goal of an abduction problem is to find a ‘solution’, i.e., an explanation for some observed symptoms. Usually, many solutions exist, and one is often interested in minimal ones only. Previous definitions of ‘solutions’ to an abduction problem tacitly made an open-world assumption. However, as far as minimality is concerned, this assumption may not always lead to the desired behaviour. To overcome this problem, we propose a new definition of solutions based on a closed-world approach. Moreover, we also introduce a new variant of minimality where only a part of the hypotheses is subject to minimization. A thorough complexity analysis reveals the close relationship between these two new notions as well as the differences compared with previous notions of solutions.
    Print ISSN: 0955-792X
    Electronic ISSN: 1465-363X
    Topics: Computer Science , Mathematics
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 8
    facet.materialart.
    Unknown
    Oxford University Press
    Publication Date: 2015-05-29
    Description: We study a collection of logics L ( T , I ) with models based on ‘dynamic I spaces’, which are finite sequences of Kripke I frames with a common domain, I being any of the normal modal systems K , K 4, T , B , S 4, KTB , KB 4 and S 5. The language of L ( T , I ) has modal connectives for ‘possibility’ and ‘necessity’, as well as temporal connectives. The semantics of L ( T , I ) can be determined through a kind of fibring over a combination of temporal and Kripke I frames corresponding to the modal system I . This article presents, in a schematic manner, tableau-based proof procedures for this class of logics. Comparisons with closely related systems are made. We briefly look at possible applications of the logics as well. The study, in fact, generalizes the work on the logic temporal rough logic (TRL) by Banerjee and Khan [ 2 ] for Pawlak's rough set theory (RST), models of which are based on dynamic S 5 spaces. The motivation behind TRL was to capture reasoning with rough sets in the scenario of a knowledge base evolving with time, when the latter is represented by a partition on the domain of discourse. RST has been generalized in many ways over the years, in particular to situations when the knowledge base is not necessarily represented by an equivalence relation, but, for instance, by tolerances or pre-orders. The logics presented here enable one to address reasoning with concepts in the context of such generalized knowledge bases evolving with time.
    Print ISSN: 0955-792X
    Electronic ISSN: 1465-363X
    Topics: Computer Science , Mathematics
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 9
    facet.materialart.
    Unknown
    Oxford University Press
    Publication Date: 2015-05-29
    Description: Motivated from reasoning in rough set theory, we have introduced and studied proof-theoretic properties of a class of logics L ( T , I ) in the first part of this article. These are logics with models based on ‘dynamic I spaces’, which are finite sequences of Kripke I frames with a common domain, I being any of the normal modal systems K , K 4, T , B , S 4, KTB , KB 4, S 5. This article presents the second part of the study on L ( T , I ), where we focus on decidability issues.
    Print ISSN: 0955-792X
    Electronic ISSN: 1465-363X
    Topics: Computer Science , Mathematics
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 10
    Publication Date: 2015-05-29
    Description: We study the expressive power of fragments of inclusion and independence logic defined by restricting the number k of universal quantifiers in formulas. Assuming the so-called strict semantics for these logics, we relate these fragments of inclusion and independence logic to sublogics $${\hbox{ ESO }}_{f}(k\forall )$$ of existential second-order logic, which in turn are known to capture the complexity classes $${\hbox{ NTIME }}_{\hbox{ RAM }}({n}^{k})$$ .
    Print ISSN: 0955-792X
    Electronic ISSN: 1465-363X
    Topics: Computer Science , Mathematics
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 11
    Publication Date: 2015-05-29
    Description: An undirected graph is commonly represented as a set of vertices and a set of vertex doubletons; but one can also represent each vertex by a finite set so as to ensure that membership mimics, over these vertex-representing sets, the edge relation of the graph. This alternative modelling, applied to connected claw-free graphs, recently gave crucial clues for obtaining simpler proofs of some of their properties (e.g. Hamiltonicity of the square of the graph). This article adds a computer-checked contribution. On the one hand, we discuss our development, by means of the Ref verifier, of two theorems on representing graphs by families of finite sets: a weaker theorem pertains to general graphs, and a stronger one to connected claw-free graphs. Before proving those theorems, we must show that every graph admits an acyclic, weakly extensional orientation, which becomes fully extensional when connectivity and claw-freeness are met. This preliminary work enables injective decoration, à la Mostowski, of the vertices by the sought-for finite sets. By this new scenario, we complement our earlier formalization with Ref of two classical properties of connected claw-free graphs. On the other hand, our present work provides another example of the ease with which graph-theoretic results are proved with the Ref verifier. For example, we managed to define and exploit the notion of connected graph without resorting to the notion of path.
    Print ISSN: 0955-792X
    Electronic ISSN: 1465-363X
    Topics: Computer Science , Mathematics
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 12
    Publication Date: 2015-05-29
    Description: The difficulty in finding analytic Gentzen sequent calculi for non-classical logics has lead to the development of many new proof frameworks (proof systems) that have been used to give analytic calculi for these logics. The multitude and diversity of such frameworks has made it increasingly important to identify their interrelationships and relative expressive power. Hypersequent and Display calculi are two widely-used proof frameworks employed to present analytic calculi for large classes of logics. In this article, we show how any hypersequent calculus can be used to construct a display calculus for the same logic. The display calculus we obtain preserves proof-theoretic properties of the original calculus including cut-elimination and the subformula property. Since the construction applies to any hypersequent calculus, this result shows that in terms of presenting logics the display calculus formalism subsumes the hypersequent calculus formalism.
    Print ISSN: 0955-792X
    Electronic ISSN: 1465-363X
    Topics: Computer Science , Mathematics
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 13
    Publication Date: 2015-05-29
    Description: Hereditarily finite sets (sets which are finite and have only hereditarily finite sets as members) are basic mathematical and computational objects, and also stand at the basis of some programming languages. We solve an open problem proposed by Kirby in 2008 concerning a recurrence relation for the cardinality $${a}_{n}$$ of the $$n$$ -th level of the adjunctive hierarchy of hereditarily finite sets; in this hierarchy, new sets are formed by the addition of a new single element drawn from the already existing sets to an already existing set. We also show that our results can be generalized to sets with atoms, or can be refined by rank, cardinality, or by the maximum level from where the new adjoined element is drawn. We also show that $${a}_{n}$$ satisfies the asymptotic formula $${a}_{n}={C}^{{2}^{n}}+O({C}^{{2}^{n-1}})$$ , for a constant $$C\approx 1.3399$$ , which is a too fast asymptotic growth for practical purposes. We thus propose a very natural variant of the adjunctive hierarchy, whose asymptotic behaviour we prove to be $$\Theta ({2}^{n})$$ .
    Print ISSN: 0955-792X
    Electronic ISSN: 1465-363X
    Topics: Computer Science , Mathematics
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 14
    Publication Date: 2015-05-29
    Description: This article continues Dietrich and List's (2010) work on propositional-attitude aggregation theory, which is a generalized unification of the judgement aggregation and probabilistic opinion-pooling literatures. We first propose an algebraic framework for an analysis of (many-valued) propositional-attitude aggregation problems. Then we shall show that systematic propositional-attitude aggregators can be viewed as homomorphisms—algebraically structure-preserving maps—in the category of Chang's (1958a, Trans. Am. Math. Soc. , 88 , 467–490) MV-algebras. (Proof idea: Systematic aggregators are induced by maps satisfying certain functional equations, which in turn can be verified to entail homomorphy identities.) Since the 2-element Boolean algebra as well as the real unit interval can be endowed with an MV-algebra structure, we obtain as natural corollaries two famous theorems: Arrow's theorem for judgement aggregation as well as McConway's (1981, J. Am. Stat. Assoc. , 76 , 410–414) characterization of linear opinion pools. Conceptually, this characterization of aggregators can be seen as justifying a certain structuralist interpretation of social choice. Technically and perhaps more importantly, it opens up a new methodology to social-choice theorists: the analysis of general aggregation problems by means of universal algebra.
    Print ISSN: 0955-792X
    Electronic ISSN: 1465-363X
    Topics: Computer Science , Mathematics
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 15
    Publication Date: 2015-05-29
    Description: In this article, first we generalize from the MV algebra [0,1] to an arbitrary MV algebra A the well-known Galois connection ( V , I ) between the powerset of each power of [0,1] and the powerset of the corresponding free MV algebra. Then, in analogy with the Nullstellensatz of classical algebraic geometry, we study the closure operators obtained by composing the functors V and I .
    Print ISSN: 0955-792X
    Electronic ISSN: 1465-363X
    Topics: Computer Science , Mathematics
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 16
    Publication Date: 2016-07-27
    Description: In this article, I offer an interpretation of cycles in Dung-style argumentation frameworks in which even length cycles are treated as dilemmas and odd length cycles as paradoxes. The different properties of cycles with different parities arising from the use of preferred semantics are argued to be coherent with this interpretation.
    Print ISSN: 0955-792X
    Electronic ISSN: 1465-363X
    Topics: Computer Science , Mathematics
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 17
    Publication Date: 2016-07-27
    Description: In abstract argumentation theory, preferred semantics has become one of the most popular approaches for determining the sets of arguments that can collectively be accepted. However, the description of preferred semantics, as it was originally stated by Dung, has a mainly technical and mathematical nature, making it difficult for lay persons to understand what the concept of preferred semantics is essentially about. In the current article, we aim to bridge the gap between mathematics and philosophy by providing a reformulation of (credulous) preferred semantics in terms of Socratic discussion. In order to do so, we first provide a (semi-)formal treatment of some of the concepts in Socratic dialogue.
    Print ISSN: 0955-792X
    Electronic ISSN: 1465-363X
    Topics: Computer Science , Mathematics
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 18
    Publication Date: 2016-07-27
    Description: Recently, stage and cf 2 semantics for abstract argumentation attracted specific attention. By distancing from the notion of defence, they are capable to select arguments out of odd-length cycles. In case of cf 2 semantics, the SCC-recursive schema guarantees that important evaluation criteria for argumentation semantics, like directionality, weak- and $$\mathcal{C}$$ $$\mathcal{F}$$ -reinstatement, are fulfilled. Beside several desirable properties, both stage and cf 2 semantics still have some drawbacks. The stage semantics does not satisfy the above mentioned evaluation criteria, whereas cf 2 semantics produces some questionable results on frameworks with cycles of length ≥ 6. Therefore, we suggest to combine stage semantics with the SCC-recursive schema of cf 2 semantics. The resulting stage 2 semantics overcomes the problems regarding cf 2 and stage semantics. We study properties of stage 2 semantics and its relations to existing semantics, show that it fulfills the mentioned evaluation criteria, study strong equivalence for stage 2 semantics and provide a comprehensive complexity analysis of the associated reasoning problems. Besides the analysis of stage 2 semantics, we also complement existing complexity results for cf 2 by an analysis of tractable fragments and fixed parameter tractability. Furthermore, we provide answer-set programming (ASP) encodings for stage 2 semantics and labelling-based algorithms for cf 2 and stage 2 semantics.
    Print ISSN: 0955-792X
    Electronic ISSN: 1465-363X
    Topics: Computer Science , Mathematics
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 19
    Publication Date: 2016-07-27
    Description: In this article, we propose a recursive semantics for warranted formulas in a general defeasible logic argumentation framework by formalizing a notion of collective (non-binary) conflict among arguments. The recursive semantics for warranted formulas is based on the intuitive grounds that if an argument is rejected, then further arguments built on top of it should also be rejected. The main characteristic of our recursive semantics is that an output (or extension) of a knowledge base is a pair consisting of a set of warranted and a set of blocked formulas. Arguments for both warranted and blocked formulas are recursively based on warranted formulas but, while warranted formulas do not generate any collective conflict, blocked conclusions do. Formulas that are neither warranted nor blocked correspond to rejected formulas. Then we extend the framework by attaching levels of preference to defeasible knowledge items and by providing a level-wise definition of warranted and blocked formulas. After we consider the warrant recursive semantics for the particular framework of Possibilistic Defeasible Logic Programming (RP-DeLP for short). Since RP-DeLP programmes may have multiple outputs, we define the maximal ideal output of an RP-DeLP programme as the set of conclusions which are ultimately warranted, and we present an algorithm for computing it in polynomial space and with an upper bound on complexity equal to P NP . Finally, we propose an efficient and scalable implementation of this algorithm using SAT encodings, and we provide an experimental evaluation when solving test sets of instances with single and multiple preference levels for defeasible knowledge.
    Print ISSN: 0955-792X
    Electronic ISSN: 1465-363X
    Topics: Computer Science , Mathematics
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 20
    Publication Date: 2016-07-27
    Description: In this article, we extend Dung's formal approach from admissibility to less demanding extension semantics allowing arguments in cycles of attacks. We present an acceptance criterion leading to the characterization of three semantics called pairwise cogency , weak cogency and cyclic cogency . Particular game-theoretic protocols allow us to identify winning strategies with extensions in different semantics. Furthermore, an algorithmic characterization of those games exhibits clearly how self-attacking or in odd-length cycles of attack can be rationally managed beyond the limits of admissibility.
    Print ISSN: 0955-792X
    Electronic ISSN: 1465-363X
    Topics: Computer Science , Mathematics
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 21
    Publication Date: 2016-07-27
    Print ISSN: 0955-792X
    Electronic ISSN: 1465-363X
    Topics: Computer Science , Mathematics
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 22
    facet.materialart.
    Unknown
    Oxford University Press
    Publication Date: 2016-07-27
    Description: This article is about busting loops in abstract argumentation networks. We propose several approaches to how to deal with networks which have loops (such as even or odd cycles) and get new extensions which are ‘in’, ‘out’ extensions, with no undecided elements.
    Print ISSN: 0955-792X
    Electronic ISSN: 1465-363X
    Topics: Computer Science , Mathematics
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 23
    Publication Date: 2016-07-27
    Description: Current approaches for giving semantics to abstract argumentation frameworks dismiss altogether any possibility of having conflicts among accepted arguments by requiring that the latter should be ‘conflict free’. In reality, however, contradictory phenomena coexist, or it may happen that one cannot make a choice between conflicting indications but still would like to keep track to all of them. For this purpose we introduce in this article a new kind of argumentation semantics, called ‘conflict-tolerant’, in which all the accepted arguments must be justified (in the sense that each one of them can be defended), but some of them may still attack each other. In terms of graphical representation of argumentation systems, where attacks are represented by directed edges, this means that the possibility of accepting ‘loops’ of arguments is not automatically ruled out without any further considerations. To provide conflict-tolerant semantics, we enhance the two standard approaches for defining coherent (conflict-free) semantics for argumentation frameworks. The extension-based approach is generalized by relaxing the ‘conflict-freeness’ requirement of the chosen sets of arguments, and the three-valued labelling approach is replaced by a four-valued labelling system that allows to capture mutual attacks among accepted arguments. We show that our setting is not a substitute of standard (conflict-free) semantics, but rather a generalized framework that accommodates both conflict-free and conflict-tolerant semantics. Moreover, the one-to-one relationship between extensions and labellings of conflict-free semantics is carried on to a similar correspondence between the extended approaches for providing conflict-tolerant semantics. Thus, in our setting as well, these are essentially two points of views for the same thing.
    Print ISSN: 0955-792X
    Electronic ISSN: 1465-363X
    Topics: Computer Science , Mathematics
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 24
    Publication Date: 2016-07-27
    Description: A special case of loops in argumentation are self-attacking arguments. While their role with respect to the ontological nature of argumentation is controversially discussed, their presence (or absence) in the abstract setting of Dung-style argumentation frameworks seems to be less crucial for semantics or fundamental properties. There are, however, a few exceptions where self-attacking arguments have essential influence. One such exception concerns characterizations of (strong) equivalence notions between argumentation frameworks. Different notions of equivalence have recently been proposed in the literature and several characterization results for different semantics have been obtained. In this article, we will survey the current state of this research direction with a particular emphasis on the effect of (dis)allowing self-conflicting arguments. We also provide some novel results for stage, eager and naive semantics in order to present a full classification of ten prominent semantics and four equivalence notions.
    Print ISSN: 0955-792X
    Electronic ISSN: 1465-363X
    Topics: Computer Science , Mathematics
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 25
    Publication Date: 2013-09-26
    Description: Arguments need to be judged against other arguments. The decision to accept or reject an argument is generally a global decision that involves examining the same question for other arguments that oppose or can defend the argument in question. This article presents the acceptability semantics for abstract argumentation that through a recursive definition gives a global assignment of the acceptable and non-acceptable subsets of arguments. This semantics stems from the aim to formalize directly the generally accepted intuition that: ‘An argument can be accepted if and only if all its challenging arguments can be rejected.’ The acceptability semantics tightly integrates the notion of defending against a challenging argument by counter-attacking it with the notion of self-defeating (or self-rejecting) arguments that (help to) bring about their own non-acceptability. The proposal is motivated by earlier studies of the semantics of Logic Programming (LP) in terms of argumentation, where the basic well founded and stable model semantics of LP can be uniformly captured using a recursively defined argumentation semantics for Negation as Failure and where these standard semantics of LP can be further extended through argumentation.
    Print ISSN: 0955-792X
    Electronic ISSN: 1465-363X
    Topics: Computer Science , Mathematics
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 26
    Publication Date: 2013-09-26
    Description: This article is concerned with the design and analysis of polynomial time algorithms for determining whether a Planar Quantified Integer Program (PQIP) is feasible. A PQIP can be described briefly as an integer program involving two variables, in which each variable can be either universally or existentially quantified. There are four types of PQIPs, depending on how the variables are quantified (existentially or universally). In this article, we present two new, simple, and efficient algorithms for the case as well as a detailed account of the complexity of the other cases. Moreover, we discuss certification with respect to the provided algorithms.
    Print ISSN: 0955-792X
    Electronic ISSN: 1465-363X
    Topics: Computer Science , Mathematics
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 27
    Publication Date: 2013-09-26
    Description: In the present article, the quantifiers over propositions are first introduced into the language for reasoning about probability, then the complexity issues for validity problems dealing with the corresponding hierarchy of probabilistic sentences are investigated. We prove, among other things, the $${\Pi }_{1}^{1}$$ -completeness for the general validity and also indicate the least level in the hierarchy for which the validity problem is undecidable.
    Print ISSN: 0955-792X
    Electronic ISSN: 1465-363X
    Topics: Computer Science , Mathematics
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 28
    facet.materialart.
    Unknown
    Oxford University Press
    Publication Date: 2013-09-26
    Description: We use mosaics to provide a simple, sound, complete and terminating tableau reasoning procedure for the temporal logic of until and since over general linear time.
    Print ISSN: 0955-792X
    Electronic ISSN: 1465-363X
    Topics: Computer Science , Mathematics
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 29
    Publication Date: 2013-09-26
    Description: The aim of what semantic science is to have scientific ontologies, data and hypotheses represented and published in machine understandable forms that enable predictions on new cases. There is much work on developing scientific ontologies and representing scientific data in terms of these ontologies. The next step is to publish hypotheses that can make (probabilistic) predictions on the published data and can be used for prediction on new cases. The published data can be used to evaluate hypotheses. To make a prediction in a particular case, hypotheses are combined to form models. This article considers feature-based semantic science where the data and new cases are described in terms of features. A prediction for a new case is made by building a model made up of hypotheses that fit together, are consistent with the ontologies used, and are adequate for the case. We give some desiderata for such models, and show how the construction of such models is a form of abduction. We provide a definition for models that satisfies these criteria and prove that it produces a coherent probability distribution over the values of interest.
    Print ISSN: 0955-792X
    Electronic ISSN: 1465-363X
    Topics: Computer Science , Mathematics
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 30
    facet.materialart.
    Unknown
    Oxford University Press
    Publication Date: 2013-09-26
    Description: In this article we present methods of transition from one perspective on logic to others, and apply this in particular to obtain a coalgebraic presentation of logic. The central ingredient in this process is to view consequence relations as morphisms in a category.
    Print ISSN: 0955-792X
    Electronic ISSN: 1465-363X
    Topics: Computer Science , Mathematics
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 31
    Publication Date: 2013-09-26
    Description: We consider the expressive power of the first-order structure 〈, C 〉 where is either of two of different domains of extended regions in Euclidean space, and C(x,y) is the topological relation ‘Region x is in contact with region y .’ We prove two main theorems: Let $$\mathcal{P}$$ [Q] be the domain of bounded, non-empty, rational polyhedra in two- or three-dimensional Euclidean space. A relation over $$\mathcal{P}$$ [Q] is definable in the structure 〈 $$\mathcal{P}$$ [Q], C 〉 if and only if is arithmetic and invariant under rational PL-homeomorphisms of the space to itself. We also extend this result to a number of other domains, including the domain of all polyhedra and the domain of semi-algebraic regions. Let $$\mathcal{R}$$ be the space of bounded, non-empty, closed regular regions in n -dimensional Euclidean space. Any analytical relation over lower dimensional (i.e. empty interior) compact point sets that is invariant under homeomorphism is implicitly definable in the structure 〈 $$\mathcal{R}$$ , C 〉.
    Print ISSN: 0955-792X
    Electronic ISSN: 1465-363X
    Topics: Computer Science , Mathematics
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 32
    Publication Date: 2013-09-26
    Description: argumentation frameworks nowadays provide the most popular formalization of argumentation on a conceptual level. Numerous semantics for this paradigm have been proposed, whereby the cf2 semantics has shown to solve particular problems concerned with odd-length cycles in such frameworks. Due to the complicated definition of this semantics it has somehow been neglected in the literature. In this article, we introduce an alternative characterization of the cf2 semantics which, roughly speaking, avoids the recursive computation of subframeworks. This facilitates further investigation steps, like a complete complexity analysis. Furthermore, we show how the notion of strong equivalence can be characterized in terms of the cf2 semantics. In contrast to other semantics, it turns out that for the cf2 semantics strong equivalence coincides with syntactical equivalence. We make this particular behaviour more explicit by defining a new property for argumentation semantics, called the succinctness property. If a semantics satisfies the succinctness property, then for every framework F , all its attacks contribute to the evaluation of at least one framework F ' containing F . We finally characterize strong equivalence also for the stage and the naive semantics. Together with known results these characterizations imply that none of the prominent semantics for abstract argumentation, except the cf2 semantics, satisfies the succinctness property.
    Print ISSN: 0955-792X
    Electronic ISSN: 1465-363X
    Topics: Computer Science , Mathematics
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 33
    Publication Date: 2013-09-26
    Description: The Argument Interchange Format (AIF) has been devised in order to support the interchange of ideas and data between different projects and applications in the area of computational argumentation. In order to support such interchange, an abstract ontology for argumentation is presented, which serves as an interlingua between various more concrete argumentation languages. In this article, we aim to give what is essentially a logical specification of the AIF ontology by mapping the ontology onto the logical ASPIC + framework for argumentation. We thus lay foundations for interrelating formal logic-based approaches to argumentation captured by the ASPIC + framework and the wider class of argumentation languages, including those that are more informal and user-orientated.
    Print ISSN: 0955-792X
    Electronic ISSN: 1465-363X
    Topics: Computer Science , Mathematics
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 34
    Publication Date: 2015-04-02
    Description: We investigate models of first-order logic designed to give semantics to reductive proof-search systems, with special attention to the so-called - and -rules controlling quantifiers. The key innovation is the use of syntax and semantics with (finitely supported) name-symmetry , in the style of nominal techniques.
    Print ISSN: 0955-792X
    Electronic ISSN: 1465-363X
    Topics: Computer Science , Mathematics
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 35
    Publication Date: 2015-04-02
    Description: In this article, we introduce a new approach of preference-based argumentation frameworks. We first introduce an abstract preference-based argumentation framework (an abstract PAF ) which handles static preferences . Naturally extending Dung's acceptability semantics, the semantics of an abstract PAF is given by $$\mathcal{P}$$ -extensions which ensure conflict-freeness w.r.t. the attack relation. Second, as the instantiation of the proposed abstract PAF , we present the non-abstract PAF along with the constrained argumentation framework ( CAF ) built from a prioritized logic program (PLP). As a result, the proposed framework is able to handle static preferences as well as integrity constraints in argumentation. Third, by providing a hierarchical PLP to deal with dynamic preferences in the context of logic programming, we extend the framework to a dynamic PAF built from a hierarchical PLP to deal with dynamic preferences in the context of argumentation. Fourth, we not only show the correspondence between stable extensions of the non-abstract argumentation framework and paraconsistent stable models of an extended logic program but also show the correspondence between the semantics of such PAF s and the semantics of the underling prioritized logic programs based on the order-preserving mapping functions. Finally, the proposed framework is also applied to interactions between agents in multi-agent systems.
    Print ISSN: 0955-792X
    Electronic ISSN: 1465-363X
    Topics: Computer Science , Mathematics
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 36
    Publication Date: 2015-04-02
    Description: Over the last decennia, many systems for formal argumentation have been defined. The problem, however, is that these systems do not always satisfy reasonable properties. In the current study, we focus on the particular property that a conflict between two arguments should not keep other unrelated arguments from becoming justified. Although this property appears obvious, it is in fact violated by several existing argumentation formalisms. In this article we examine what exactly goes wrong and how things can be improved.
    Print ISSN: 0955-792X
    Electronic ISSN: 1465-363X
    Topics: Computer Science , Mathematics
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 37
    Publication Date: 2016-03-30
    Print ISSN: 0955-792X
    Electronic ISSN: 1465-363X
    Topics: Computer Science , Mathematics
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 38
    Publication Date: 2016-03-30
    Description: A class of axiomatic theories with arbitrary quantifier alternations is identified and a conversion to normal form is provided in terms of generalized geometric implications . The class is also characterized in terms of Glivenko classes as those first-order formulas that do not contain implications or universal quantifiers in the negative part. It is shown how the methods of proof analysis can be extended to cover such axioms by means of conversion to systems of rules . The structural properties for the resulting extensions of sequent calculus are established and a generalization of the first-order Barr theorem is shown to follow as an immediate application. The method is also applied to obtain complete labelled proof systems for logics defined through their relational semantics. In particular, the method provides analytic proof systems for all the modal logics in the Sahlqvist fragment.
    Print ISSN: 0955-792X
    Electronic ISSN: 1465-363X
    Topics: Computer Science , Mathematics
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 39
    Publication Date: 2016-03-30
    Description: It has been shown that linear logic can be successfully used as a framework for both specifying proof systems for a number of logics, as well as proving fundamental properties about the specified systems. This article shows how to extend the framework with subexponentials in order to declaratively encode a wider range of proof systems, including a number of non-trivial proof systems such as multi-conclusion intuitionistic logic, classical modal logic S4, intuitionistic Lax logic, and Negri's labelled proof systems for different modal logics. Moreover, we propose methods for checking whether an encoded proof system has important properties, such as if it admits cut-elimination, the completeness of atomic identity rules, and the invertibility of its inference rules. Finally, we present a tool implementing some of these specification/verification methods.
    Print ISSN: 0955-792X
    Electronic ISSN: 1465-363X
    Topics: Computer Science , Mathematics
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 40
    Publication Date: 2016-03-30
    Description: The sequent calculus is often criticized for requiring proofs to contain large amounts of low-level syntactic details that can obscure the essence of a given proof. Because each inference rule introduces only a single connective, sequent proofs can separate closely related steps—such as instantiating a block of quantifiers—by irrelevant noise. Moreover, the sequential nature of sequent proofs forces proof steps that are syntactically non-interfering and permutable to nevertheless be written in some arbitrary order. The sequent calculus thus lacks a notion of canonicity : proofs that should be considered essentially the same may not have a common syntactic form. To fix this problem, many researchers have proposed replacing the sequent calculus with proof structures that are more parallel or geometric. Proof-nets, matings and atomic flows are examples of such revolutionary formalizms. We propose, instead, an evolutionary approach to recover canonicity within the sequent calculus, which we illustrate for classical first-order logic. The essential element of our approach is the use of a multi-focused sequent calculus as the means for abstracting away low-level details from classical cut-free sequent proofs. We show that, among the multi-focused proofs, the maximally multi-focused proofs that collect together all possible parallel foci are canonical. Moreover, if we start with a certain focused sequent proof system, such proofs are isomorphic to expansion proofs —a well known, minimalistic and parallel generalization of Herbrand disjunctions—for classical first-order logic. This technique appears to be a systematic way to recover the ‘essence of proof’ from within sequent calculus proofs.
    Print ISSN: 0955-792X
    Electronic ISSN: 1465-363X
    Topics: Computer Science , Mathematics
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 41
    facet.materialart.
    Unknown
    Oxford University Press
    Publication Date: 2016-03-30
    Description: Girard showed that every type of sort * (i.e. every proposition) is inhabited in U. Barendregt states without proof that every type of sort (i.e. every domain) is also inhabited in the system. This article shows that the second statement is not the case by giving a partial translation from U to 2.
    Print ISSN: 0955-792X
    Electronic ISSN: 1465-363X
    Topics: Computer Science , Mathematics
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 42
    Publication Date: 2016-03-30
    Description: Coinductive definitions, such as that of an infinite stream, may often be described by elegant logic programs, but ones for which SLD-refutation is of no value as SLD-derivations fall into infinite loops. Such definitions give rise to questions of lazy corecursive derivations and parallelism, as execution of such logic programs can have both recursive and corecursive features at once. Observational and coalgebraic semantics have been used to study them abstractly. The programming developments have often occurred separately and have usually been implementation-led. Here, we give a coherent semantics-led account of the issues, starting with abstract category theoretic semantics, developing coalgebra to characterize naturally arising trees and proceeding towards implementation of a new dialect, CoALP, of logic programming, characterised by guarded lazy corecursion and parallelism.
    Print ISSN: 0955-792X
    Electronic ISSN: 1465-363X
    Topics: Computer Science , Mathematics
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 43
    Publication Date: 2016-03-30
    Description: We describe an approach to automatically prove the functional correctness of pointer programs that involve iteration and recursion. Building upon separation logic, our approach has been implemented as a tightly integrated tool chain incorporating a novel combination of proof planning and invariant generation. Starting from shape analysis, performed by the Smallfoot static analyser, we have developed a proof strategy that combines shape and functional aspects of the verification task. By focusing on both iterative and recursive code, we have had to address two related invariant generation tasks, i.e. loop and frame invariants. We deal with both tasks uniformly using an automatic technique called term synthesis , in combination with the IsaPlanner/Isabelle theorem prover. In addition, where verification fails, we attempt to overcome failure by automatically generating missing preconditions. We present in detail our experimental results. Our approach has been evaluated on a range of examples, drawn in part from a functional extension to the Smallfoot corpus.
    Print ISSN: 0955-792X
    Electronic ISSN: 1465-363X
    Topics: Computer Science , Mathematics
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 44
    facet.materialart.
    Unknown
    Oxford University Press
    Publication Date: 2016-03-30
    Description: Nominal logic is a variant of first-order logic that provides support for reasoning about bound names in abstract syntax. A key feature of nominal logic is the new-quantifier, which quantifies over fresh names (names not appearing in any values considered so far). Previous attempts have been made to develop convenient rules for reasoning with the new-quantifier, but we argue that none of these attempts is completely satisfactory. In this article we develop a new sequent calculus for nominal logic in which the rules for the new-quantifier are much simpler than in previous attempts. We also prove several structural and metatheoretic properties, including cut-elimination, consistency and equivalence to Pitts' axiomatization of nominal logic.
    Print ISSN: 0955-792X
    Electronic ISSN: 1465-363X
    Topics: Computer Science , Mathematics
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 45
    Publication Date: 2016-03-30
    Description: The paper surveys several views of proof-theoretic semantics and classifies them in accordance to the choice of which of the rules of a meaning-conferring natural-deduction system determines the meaning of the defined expression. Then, in contrast to the traditional approach that regards the rules as determining meaning implicitly, the paper proposes an explicit definition of meaning in terms of rules, appealing to collections of canonical derivations. A certain claim about a conclusion from the non-eliminability of the rules that are not meaning conferring is refuted, and an alternative explanation of non-eliminability is proposed.
    Print ISSN: 0955-792X
    Electronic ISSN: 1465-363X
    Topics: Computer Science , Mathematics
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 46
    Publication Date: 2016-03-30
    Description: In this paper we show how Dummett-Prawitz-style proof-theoretic semantics has to be modified in order to cope with paradoxical phenomena. It will turn out that one of its basic tenets has to be given up, namely the definition of the correctness of an inference as validity preservation. As a result, the notions of an argument being valid and of an argument being constituted by correct inference rules will no more coincide. The gap between the two notions is accounted for by introducing the distinction between sense and denotation in the proof-theoretic-semantic setting.
    Print ISSN: 0955-792X
    Electronic ISSN: 1465-363X
    Topics: Computer Science , Mathematics
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 47
    facet.materialart.
    Unknown
    Oxford University Press
    Publication Date: 2016-03-30
    Description: For centuries, the highest level of mathematics has been seen as an isolated creative activity, to produce a proof for review and acceptance by research peers. Mathematics is now at a remarkable inflexion point, with new technology radically extending the power and limits of individuals. ‘Crowdsourcing’ pulls together diverse experts to solve problems; symbolic computation tackles huge routine calculations; and computers, using programs designed to verify hardware, check proofs that are just too long and complicated for any human to comprehend. ‘Social machines’ are new paradigm, identified by Berners-Lee, for viewing a combination of people and computers as a single problem-solving entity. This paper outlines a research agenda for a new vision of a mathematics social machine, a combination of people, computers, and archives to create and apply mathematics, and places it in the context of verification research, computational logic and Roy Dyckhoff's pioneering work on computer proof.
    Print ISSN: 0955-792X
    Electronic ISSN: 1465-363X
    Topics: Computer Science , Mathematics
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 48
    Publication Date: 2016-03-30
    Description: We recall that SBV, a proof system developed under the methodology of deep inference, extends multiplicative linear logic with the self-dual non-commutative logical operator Seq. We introduce SBVB that extends SBV by adding the self-dual binder Sdb on names. The system SBVB is consistent because we prove that (the analogous of) cut-elimination holds for it. Moreover, the resulting interplay between Seq and Sdb can model β-reduction of linear -calculus inside the cut-free subsystem BVB of SBVB. The long-term aim is to keep developing a programme whose goal is to give pure logical accounts of computational primitives under the proof-search-as-computation analogy, by means of minimal and incremental extensions of SBV.
    Print ISSN: 0955-792X
    Electronic ISSN: 1465-363X
    Topics: Computer Science , Mathematics
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 49
    Publication Date: 2016-03-30
    Description: This article presents a self-contained proof of the strong completeness of the labelled tableaux method for partial monoidal Boolean BI: if a formula has no tableau proof then there exists a counter-model for it which is simple. Simple counter-models are those which are generated from the specific constraints that occur during the tableaux proof-search process. As a companion to this article, we provide a complete formalization of this result in Coq and discuss some of its implementation details. The Coq code is distributed under a free software license and is accessible at http://www.loria.fr/~larchey/BBI .
    Print ISSN: 0955-792X
    Electronic ISSN: 1465-363X
    Topics: Computer Science , Mathematics
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 50
    Publication Date: 2015-05-29
    Description: In a recent paper [ Journal of Logic and Computation , forthcoming (2014); doi: 10.1093/logcom/ext009 ], it was claimed that a universal algebraic approach to general aggregation theory based on MV-homomorphisms could even cover linear probabilistic opinion pooling. This is not so, however. The reason is that there are no non-trivial homomorphisms from direct powers of the standard MV-algebra onto the standard MV-algebra itself; an analytic proof thereof is given in this note.
    Print ISSN: 0955-792X
    Electronic ISSN: 1465-363X
    Topics: Computer Science , Mathematics
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 51
    facet.materialart.
    Unknown
    Oxford University Press
    Publication Date: 2015-05-29
    Description: We prove two new results about logics involving updates and common knowledge. The first result is that the logic $${\mathcal{L}}_{\hbox{ AU }*}$$ using Arrow Common Knowledge is more expressive than the logic $$\mathcal{L}$$ AR using Relativized Common Knowledge. The second result is that the logic $$\mathcal{L}$$ AUC using Arrow Updates and normal Common Knowledge is equally expressive as $${\mathcal{L}}_{\hbox{ AU }*}$$ . Together with previously known results this fully determines the expressivity landscape of all logics involving any combination of normal Common Knowledge (C), Relativized Common Knowledge (R), Arrow Common Knowledge (U*), Public Announcements (P) and Arrow Updates (U).
    Print ISSN: 0955-792X
    Electronic ISSN: 1465-363X
    Topics: Computer Science , Mathematics
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 52
    facet.materialart.
    Unknown
    Oxford University Press
    Publication Date: 2015-05-29
    Description: In pedagogical formal systems one needs to systematically give examples of hypotheses made. This essential characteristic is not the only one needed, and we have given in a previous work a formal definition of pedagogical subsystems of the Calculus of Constructions (CC) summing up precisely the expected properties. The purpose of this definition was to give a solid guideline for the study of formal pedagogy in systems of the -cube for which CC is the most powerful instance. Indeed pedagogical formal system have logical and computational meanings: the absence of negation at logical side; and a property of usefulness of the typed functions, i.e. to any function can be given a well-typed argument. Here we give such a pedagogical subsystem of CC and we show it corresponds to the second-order pedagogical -calculus P-Prop 2 of Colson and Michel. Actually our system is an improvement of the presentation of P-Prop 2 : only one rule is constrained and there is no addition to the calculus (neither constant nor rules). Thus it illustrates the definition and proves its appropriateness. Along the way we define a natural intermediate formalism for studying formal pedagogy where examples are made explicit into the judgements. And finally we study the type-checking problem for those pedagogical calculi of second order.
    Print ISSN: 0955-792X
    Electronic ISSN: 1465-363X
    Topics: Computer Science , Mathematics
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 53
    Publication Date: 2016-05-29
    Description: We study a linear temporal logic LTLNT with non-transitive time (with NEXT and UNTIL) and possible interpretations for logical knowledge operations in this approach. We assume time to be non-transitive, linear and discrete, it is a major innovative part of our article. Motivation for our approach that time might be non-transitive and comments on possible interpretations of logical knowledge operations are given. The main result of Section 5 is a solution of the decidability problem for LTLNT , we find and describe in details the decision algorithm. In Section 6 we introduce non-transitive linear temporal logic LTLNT(m) with uniform bound ( m ) for non-transitivity. We compare it with standard linear temporal logic LTL and the logic LTLNT —where non-transitivity has no upper bound—and show that LTLNT may be approximated by logics LTLNT(m) . Concluding part of the article contains a list of open interesting problems.
    Print ISSN: 0955-792X
    Electronic ISSN: 1465-363X
    Topics: Computer Science , Mathematics
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 54
    Publication Date: 2016-05-29
    Description: We introduce Description Logics of Context (DLCs)—an extension of Description Logics (DLs) for context-based reasoning. Our approach descends from J. McCarthy's tradition of treating contexts as formal objects over which one can quantify and express first-order properties. DLCs are founded in two-dimensional possible world semantics, where one dimension represents a usual object domain and the other a domain of contexts, and accommodate two interacting DL languages—the object and the context language—interpreted over their respective domains. Effectively, DLCs comprise a family of two-sorted , two-dimensional combinations of pairs of DLs. We argue that this setup ensures a well-grounded, generic framework for capturing and studying mechanisms of contextualization in the DL paradigm. As the main technical contribution, we prove 2ExpTime-completeness of the satisfiability problem in the maximally expressive DLC, based on the DL . As an interesting corollary, we show that under certain conditions this result holds also for a range of two-dimensional DLs, including the prominent .
    Print ISSN: 0955-792X
    Electronic ISSN: 1465-363X
    Topics: Computer Science , Mathematics
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 55
    facet.materialart.
    Unknown
    Oxford University Press
    Publication Date: 2016-05-29
    Description: We show that every constraint satisfaction problem (CSP) over a fixed constraint language that has bounded relational width has also relational width (2,3). Together with known results this gives a trichotomy: a CSP has either relational width 1, or relational width (2,3) (and no smaller relational width), or does not have bounded relational width. A consequence of this result is that if $$\Gamma $$ is a finite constraint language containing relations of arity at most $$k$$ , then the CSP over $$\Gamma $$ either cannot be solved by a Datalog program, or can be solved by a Datalog program consisting of rules with at most $$\mathrm{max}\{3,k\}$$ variables and at most 2 variables in the head.
    Print ISSN: 0955-792X
    Electronic ISSN: 1465-363X
    Topics: Computer Science , Mathematics
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 56
    Publication Date: 2016-05-29
    Description: Recent counterexamples show that Harmonic Grammar (HG) error-driven learning (with the classical Perceptron reweighing rule) is not robust to noise and does not tolerate the stochastic implementation (Magri 2014, MS). This article guarantees that no analogous counterexamples are possible for proper Optimality Theory (OT) error-driven learners. In fact, a simple extension of the OT convergence analysis developed in the literature (Tesar and Smolensky 1998, Linguist. Inq ., 29 , 229–268; Boersma 2009, Linguist. Inq ., 40 , 667–686; Magri 2012, Phonology , 29 , 213–269) is shown to ensure stochastic tolerance and noise robustness of the OT learner. Implications for the comparison between the HG and OT implementations of constraint-based phonology are discussed.
    Print ISSN: 0955-792X
    Electronic ISSN: 1465-363X
    Topics: Computer Science , Mathematics
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 57
    Publication Date: 2016-05-29
    Description: We show that linear-time temporal logic over concrete domains made of finite strings and the prefix relation admits a PS pace -complete satisfiability problem. Actually, we extend a known result with the concrete domain made of the set of natural numbers and the greater than relation (corresponding to the singleton alphabet case) and we solve an open problem mentioned in several publications. Since the prefix relation is not a total ordering, it is not possible to take advantage of existing techniques dedicated to temporal logics with concrete domains that are essentially linearly ordered structures. Instead, we introduce an adequate encoding of string constraints into length constraints that allows us to reduce the problem on strings to the problem on natural numbers. To do so, we also propose an extended version of the logic on strings that is able to compare lengths of longest common prefixes and for which the satisfiability problem is shown in PS pace . Finally, we show how to lift the result for the branching-time case in order to get decidability when the underlying temporal logic is CTL*.
    Print ISSN: 0955-792X
    Electronic ISSN: 1465-363X
    Topics: Computer Science , Mathematics
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 58
    facet.materialart.
    Unknown
    Oxford University Press
    Publication Date: 2016-05-29
    Description: Symmetric Datalog, a fragment of the logic programming language Datalog, is conjectured to capture all constraint satisfaction problems (CSP) in L . Therefore developing tools that help us understand whether or not a CSP can be defined in symmetric Datalog is an important task. It is widely known that a CSP is definable in Datalog and linear Datalog if and only if that CSP has bounded treewidth and bounded pathwidth duality, respectively. In the case of symmetric Datalog, Bulatov, Krokhin and Larose ask for such a duality (2008, Vol. 5250 of LNCS , 93–124). We provide two such dualities, and give applications. In particular, we give a short and simple new proof of the result of Dalmau and Larose that ‘Maltsev + Datalog symmetric Datalog’ (2008, IEEE Symposium on LICS , 297–306). In the second part of the article, we provide some evidence for the conjecture of Dalmau (2002, Proc. ICALP , 414–425) that every CSP in NL is definable in linear Datalog. Our results also show that a wide class of CSPs–CSPs which do not have bounded pathwidth duality (e.g. the P -complete H orn -3S at problem)–cannot be defined by any polynomial size family of monotone read-once non-deterministic branching programs.
    Print ISSN: 0955-792X
    Electronic ISSN: 1465-363X
    Topics: Computer Science , Mathematics
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 59
    Publication Date: 2016-05-29
    Description: The original unification algorithm for F-Logic molecules presented by Kifer et al . 1995, contains a mistake. We identify the mistake and demonstrate it through two examples, suggest a solution to the problem in the original algorithm and prove that the resulting algorithm correctly unifies F-Logic molecules.
    Print ISSN: 0955-792X
    Electronic ISSN: 1465-363X
    Topics: Computer Science , Mathematics
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 60
    Publication Date: 2016-05-29
    Description: We define and develop the concept of quasi-variety for models of hybrid logics and we apply this for determining initial semantics for classes of hybrid logics theories. The hybrid logic is considered here in a very general sense, internal to abstract institutions (in the sense of the so-called institution theory of Goguen and Burstall). This means our result is applicable to a wide variety of hybrid logics including, e.g. those resulting from the various kinds of combinations between conventional hybrid logics and various other logical systems.
    Print ISSN: 0955-792X
    Electronic ISSN: 1465-363X
    Topics: Computer Science , Mathematics
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 61
    Publication Date: 2016-05-29
    Description: We consider the language with temporal operators G,H and coderivative operator [d] . G means ‘always in the future’, H means ‘always in the past’ and [d] means ‘around now but possibly not now’. We finitely axiomatize the logic of this language interpreted over the real line, we prove that this logic is PSPACE-complete, and that it is neither strongly complete nor Kripke-complete (and consequently that it fails the finite model property).
    Print ISSN: 0955-792X
    Electronic ISSN: 1465-363X
    Topics: Computer Science , Mathematics
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 62
    Publication Date: 2015-05-29
    Print ISSN: 0955-792X
    Electronic ISSN: 1465-363X
    Topics: Computer Science , Mathematics
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 63
    Publication Date: 2015-05-29
    Description: We consider intermediate predicate logics defined by fixed well-ordered (or dually well-ordered) linear Kripke frames with constant domains where the order-type of the well-order is strictly smaller than . We show that two such logics of different order-type are separated by a first-order sentence using only one monadic predicate symbol. Previous results by Minari, Takano and Ono, as well as the second author, obtained the same separation but relied on the use of predicate symbols of unbounded arity.
    Print ISSN: 0955-792X
    Electronic ISSN: 1465-363X
    Topics: Computer Science , Mathematics
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 64
    Publication Date: 2015-05-29
    Description: Motivated by applications in databases, this article considers various fragments of the calculus of binary relations. The fragments are obtained by leaving out, or keeping in, some of the standard operators, along with some derived operators such as set difference, projection, coprojection and residuation. For each considered fragment, a characterization is obtained for when two given binary relational structures are indistinguishable by expressions in that fragment. The characterizations are based on appropriately adapted notions of simulation and bisimulation.
    Print ISSN: 0955-792X
    Electronic ISSN: 1465-363X
    Topics: Computer Science , Mathematics
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 65
    Publication Date: 2015-05-29
    Description: Working jointly in the equivalent categories of MV-algebras and lattice-ordered abelian groups with strong order unit (for short, unital -groups), we prove that isomorphism is a sufficient condition for a separating subalgebra A of a finitely presented algebra F to coincide with F . The separation and isomorphism conditions do not individually imply A = F . Various related problems, like the separation property of A , or A F (for A a separating subalgebra of F ), are shown to be (Turing-)decidable. We use tools from algebraic topology, category theory, polyhedral geometry and computational algebraic logic.
    Print ISSN: 0955-792X
    Electronic ISSN: 1465-363X
    Topics: Computer Science , Mathematics
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 66
    Publication Date: 2015-05-29
    Description: Mobile ad hoc networks are networks that allow (mobile) users to communicate in heterogeneous environments without relying on a fixed infrastructure, examples of which are mobile communication in large urban spaces or in public transportation. Due to their many advantages, such as decentralization, independence of communication infrastructure, flexibility etc., their field of use steadily increases. However, networks of this kind also raise new problems related to, for example, routing and data delivery, security and privacy, trust and usability. In this article, we propose a formal model of mobile ad hoc networks and address questions regarding optimal and stable network topologies. In particular, stability is important to ensure that communication is reliable and that applications designed for such networks are accepted by the users. We analyse stability from a game theoretic point of view, and propose a non-cooperative as well as a cooperative modelling. Moreover, we allow users to express constraints on how their communication should be handled in the network in order to ensure user constraints, e.g. related to privacy and security. For this purpose we use the temporal logic CTL . Finally, we analyse the complexity of associated verification and synthesis problems regarding optimal/stable network topologies.
    Print ISSN: 0955-792X
    Electronic ISSN: 1465-363X
    Topics: Computer Science , Mathematics
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 67
    Publication Date: 2015-05-29
    Description: A variety of problems emerged investigating electronic circuits, computer devices and cellular automata motivated a number of attempts to create a differential and integral calculus for Boolean functions. In the present article, we extend this kind of calculus in order to include the semantic of classical logical operations. We show that this extension to logics is strongly helped if we submerge the elementary logical calculus in a matrix–vector formalism that naturally includes a kind of fuzzy-logic. In this way, guided by the laws of matrix algebra, we can construct compact representations for the derivatives and the integrals of logical functions. Inside this semantic-algebraic calculus, we obtain expressions for the derivatives of some of the basic logical operations and show the general way to obtain the derivatives of any well-formed formula of propositional calculus. We show that some of the basic tautologies ( Excluded middle, Modus ponens, Hypothetical syllogism ) are members of a kind of hierarchical system linked by the differentiation algorithm. In addition using the logical derivatives we show that relatively complex formulas can collapse in simple expressions that reveal clearly their hidden logical meaning. The search for the antiderivatives produces naturally an integral calculus. Within this logical formalism an indefinite integral can always be found for any logical expression. Moreover, particular integrals can be constructed based on detachment properties that lead to logical expressions of growing complexity. We show that these particular integrals have some similarities with the ‘generalizing deduction’ procedures investigated by Łukasiewicz.
    Print ISSN: 0955-792X
    Electronic ISSN: 1465-363X
    Topics: Computer Science , Mathematics
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 68
    Publication Date: 2015-05-29
    Description: In this note we interpret Voevodsky's Univalence Axiom in the language of (abstract) model categories. We then show that any posetal locally Cartesian closed model category $$\mathcal{Q}$$ t in which the mapping Hom ( w ) ( Z x B , C ): $$\mathcal{Q}$$ t -〉 Sets is functorial in Z and represented in $$\mathcal{Q}$$ t satisfies our homotopy version of the Univalence Axiom, albeit in a rather trivial way. This work was motivated by a question reported in [ 2 ], asking for a model of the Univalence Axiom not equivalent to the standard one.
    Print ISSN: 0955-792X
    Electronic ISSN: 1465-363X
    Topics: Computer Science , Mathematics
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 69
    facet.materialart.
    Unknown
    Oxford University Press
    Publication Date: 2015-05-29
    Description: Paraconsistent many-valued logics are known to be useful for describing inconsistency-tolerant and uncertain reasoning more appropriately than logics that are non-paraconsistent and two-valued. Shramko-Wansing's trilattice logics are paraconsistent sixteen-valued logics based on the algebraic structures of trilattices that can suitably represent generalized truth values. In this article, an alternative new proof of the cut-elimination and completeness theorems for such a trilattice logic is obtained using two embedding theorems. The Craig interpolation and Maksimova separation theorems for this logic are also proved using the same embedding theorems. The results on Craig interpolation and Maksimova separation are new results of this article. Moreover, the above mentioned results are extended to a temporal extension of the trilattice logic. The results on the temporal extension are also new contribution of this article.
    Print ISSN: 0955-792X
    Electronic ISSN: 1465-363X
    Topics: Computer Science , Mathematics
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 70
    facet.materialart.
    Unknown
    Oxford University Press
    Publication Date: 2015-01-29
    Description: One of the natural objectives of the field of the social networks is to predict agents' behaviour. To better understand the spread of various products through a social network (Apt and Markakis (2011, Lecture Notes in Computer Science , pp. 212–223)) introduced a threshold model, in which the nodes influenced by their neighbours can adopt one out of several alternatives. To analyse the consequences of such product adoption we associate here with each such social network a natural strategic game between the agents. In these games the payoff of each player weakly increases when more players choose his strategy, which is exactly opposite to the congestion games. The possibility of not choosing any product results in two special types of (pure) Nash equilibria. We show that such games may have no Nash equilibrium and that determining an existence of a Nash equilibrium, also of a special type, is NP-complete. This implies the same result for a more general class of games, namely polymatrix games. The situation changes when the underlying graph of the social network is a directed acyclic graph, a simple cycle, or, more generally, has no source nodes. For these three classes we determine the complexity of an existence of (a special type of) Nash equilibria. We also clarify for these categories of games the status and the complexity of the finite best response property and the finite improvement property (FIP). Further, we introduce a new property of the uniform FIP which is satisfied when the underlying graph is a simple cycle, but determining it is co-NP-hard in the general case and also when the underlying graph has no source nodes. The latter complexity results also hold for the property of being a weakly acyclic game.
    Print ISSN: 0955-792X
    Electronic ISSN: 1465-363X
    Topics: Computer Science , Mathematics
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 71
    Publication Date: 2015-01-29
    Description: We consider the Gödel bi-modal logic determined by fuzzy Kripke models where both the propositions and the accessibility relation are infinitely valued over the standard Gödel algebra [0,1], and prove strong completeness of the Fischer Servi intuitionistic modal logic IK plus the prelinearity axiom with respect to this semantics. We axiomatize also the bi-modal analogues of classical T , S 4 and S 5, obtained by restricting to models over frames satisfying the [0,1]-valued versions of the structural properties which characterize these logics. As an application of the completeness theorems we obtain a representation theorem for bi-modal Gödel algebras.
    Print ISSN: 0955-792X
    Electronic ISSN: 1465-363X
    Topics: Computer Science , Mathematics
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 72
    Publication Date: 2015-01-29
    Description: We introduce modal compact Hausdorff spaces as generalizations of modal spaces, and show these are coalgebras for the Vietoris functor on compact Hausdorff spaces. Modal compact regular frames and modal de Vries algebras are introduced as algebraic counterparts of modal compact Hausdorff spaces, and dualities are given for the categories involved. These extend the familiar Isbell and de Vries dualities for compact Hausdorff spaces, as well as the duality between modal spaces and modal algebras. As the first step in the logical treatment of modal compact Hausdorff spaces, a version of Sahlqvist correspondence is given for the positive modal language.
    Print ISSN: 0955-792X
    Electronic ISSN: 1465-363X
    Topics: Computer Science , Mathematics
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 73
    Publication Date: 2015-01-29
    Description: We present a contraction-free sequent calculus GS4 for the modal logic S4 such that all the rules are decreasing and enjoy the subformula property. We also introduce a refutation calculus RS4 with the same properties of GS4 . We provide a proof search algorithm that, given a sequent , returns either a proof of in GS4 or a refutation of in RS4 . From a refutation of , we can generate an S4 -model of .
    Print ISSN: 0955-792X
    Electronic ISSN: 1465-363X
    Topics: Computer Science , Mathematics
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 74
    Publication Date: 2015-01-29
    Description: The constructor-based logics constitute the logical foundation of the so-called OTS/CafeOBJ method, a modelling, specification and verification method of the observational transition systems. The important role played in algebraic specifications by the initial algebras semantics is well known. Free models along presentation morphisms provide semantics for the modules with initial denotation in structured specification languages. Following Goguen and Burstall, the notion of logical system over which we build specifications is formalized as an institution. The present work is an institution-independent study of the existence of free models along sufficient complete presentation morphisms in logics with constructors in the signatures.
    Print ISSN: 0955-792X
    Electronic ISSN: 1465-363X
    Topics: Computer Science , Mathematics
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 75
    Publication Date: 2015-01-29
    Description: Logical Systems are paramount to almost every subject in computer science. This vast number of application areas had a deep influence on us and thus on how we perceive what a formal specification of a logical system should be. Lawvere's (1963, Proc. Natl Acad. Sci ., 50 , 869–872; 2006, Theor. Appl. Categor ., 16 , 1–16) essential idea is that the fundamental relationship between syntax and semantics can be precisely formulated by adjoint functors . In this work, we show that Institutions from Goguen and Burstall (1992, J. ACM , 39 , 95–146) and Entailment Systems from Meseguer (1989, ‘General logics’ in Logic Colloquium ’ 87, 275–329) are in its essence, a family of local adjoint situations between the syntactical and semantical aspects underlying these systems. These abstractions are named Indexed Frames . Also, from a categorical perspective, Tarski's (1930, Fundamentale Begriffe der Methodologie der Deduktiven Wissenschaften I. Monatshefte fur Mathematik und Physik , 37 , 361–404) consequence operator can be formalized as Indexed Closure Operators , a construction that maps each language to the corresponding co-monad. Finally, in the framework of preorder categories, both concepts, Indexed Frames and Indexed Closure Operators are equivalent.
    Print ISSN: 0955-792X
    Electronic ISSN: 1465-363X
    Topics: Computer Science , Mathematics
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 76
    facet.materialart.
    Unknown
    Oxford University Press
    Publication Date: 2015-01-29
    Description: We introduce a reactive variant of SDL (standard deontic logic): SDLR1 (reactive standard deontic logic). Given a Kripkean view on the semantics of SDL in terms of directed graphs where arrows -〉 represent the accessibility relation between worlds, reactive models add two elements: arrows -〉 are labelled as ‘active’ or ‘inactive’, and double arrows connect arrows, e.g. ( x 1 -〉 x 2 ) ( x 3 -〉 x 4 ). The idea is that passing through x 1 -〉 x 2 activates a switch represented by that inverts the label of x 3 -〉 x 4 and hence activates respectively deactivates this arrow. This allows to introduce two modalities: is the usual KD -modality of SDL and operates on the Kripkean graph where all labels and double arrows are ignored, while Ø takes them into account. We demonstrate that RSDL1 allows for an intuitive interpretation of ‘ought’. The logic can handle contrary-to-duty cases such as several instantiations of the Chisholm set in a paradox-free way by means of using double arrows and annotations to block and give access to ideal worlds.
    Print ISSN: 0955-792X
    Electronic ISSN: 1465-363X
    Topics: Computer Science , Mathematics
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 77
    Publication Date: 2015-01-29
    Description: The purpose of this contribution is to set up a language to evaluate the results of concerted action among interdependent agents against predetermined properties that we can recognize as desirable from a deontic point of view. Unlike the standard view of logics to reason about coalitionally rational action, the capacity of a set of agents to take a rational decision will be restricted to what we will call agreements , which can be seen as solution concepts to a dependence structure present in a certain game. The language will identify those agreements that act accordingly or disaccordingly with the desirable properties arbitrarily set up in the beginning, and will reveal, by logical reasoning, a variety of structural properties of this type of collective action.
    Print ISSN: 0955-792X
    Electronic ISSN: 1465-363X
    Topics: Computer Science , Mathematics
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 78
    Publication Date: 2012-09-25
    Description: This article proposes an abstract framework for argumentation-based negotiation in which the impact of exchanging arguments on agents' theories is formally described, the different types of solutions in negotiation are investigated, and the added value of argumentation in negotiation dialogues is analysed. We study when, how and to which extent an exchange of arguments can be beneficial in negotiation. The results show that argumentation can improve the quality of an outcome but never decrease it.
    Print ISSN: 0955-792X
    Electronic ISSN: 1465-363X
    Topics: Computer Science , Mathematics
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 79
    Publication Date: 2012-09-25
    Description: Decision making is usually based on the comparative evaluation of different options by means of a decision criterion. Recently, the qualitative pessimistic criterion was articulated in terms of a four-step argumentation process: (i) to build arguments in favour/against each option, (ii) to compare and evaluate those arguments, (iii) to assign a status for each option, and (iv) to rank order the options on the basis of their status. Thus, the argumentative counter-part of the pessimistic criterion provides not only the ‘best’ option to the user but also the reasons justifying this recommendation. The aim of this article is to study the dynamics of this argumentation model. The idea is to study how the ordering on options changes in light of a new argument. For this purpose, we study under which conditions an option may change its status, and under which conditions the new argument has no impact on the status of options, and consequently, on the ordering. This amounts to study how the acceptability of arguments evolves when the decision system is extended by new arguments. In the article, we focus on two acceptability semantics the skeptical grounded semantics and the credulous preferred semantics.
    Print ISSN: 0955-792X
    Electronic ISSN: 1465-363X
    Topics: Computer Science , Mathematics
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 80
    Publication Date: 2012-09-25
    Description: We introduce expressible preferential logics, whose preference relations can be defined by some abstract logic. Abstract logics not only allow one to describe preference relations, but also classes of abstract preferential logics and give general proofs for properties common to all logics in these classes. Our approach follows that of Abstract Model Theory. We show that some well-known non-monotonic logics are preferential. We prove that they are elementary, which means that their preference relation can be defined in first-order logic. We study expressiveness and definability results for wide classes of abstract preferential logics in the spirit of Universal Logic. We present a collapse result for expressible preferential logics. We prove that, for a class of expressible preferential logics, if the class of minimal models of a finite set of sentences is - $$\mathcal{L}$$ -expressible, then it is $$\mathcal{L}$$ -expressible, i.e. such class of models can be finitely axiomatized in $$\mathcal{L}$$ . Using this result, we show that under certain conditions one can axiomatize the class C of minimal models of a finite set of sentences where some symbol P is defined using that set and an explicit definition for this symbol.
    Print ISSN: 0955-792X
    Electronic ISSN: 1465-363X
    Topics: Computer Science , Mathematics
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 81
    Publication Date: 2012-09-25
    Description: In this article, we investigate the complexity of abduction, a fundamental and important form of non-monotonic reasoning. Given a knowledge base explaining the world's behaviour, it aims at finding an explanation for some observed manifestation. In this article, we consider propositional abduction, where the knowledge base and the manifestation are represented by propositional formulæ. The problem of deciding whether there exists an explanation has been shown to be $${\Sigma }_{2}^{\hbox{ p }}$$ -complete in general. We focus on formulæ in which the allowed connectives are taken from certain sets of Boolean functions. We consider different variants of the abduction problem in restricting both the manifestations and the hypotheses. For all these variants, we obtain a complexity classification for all possible sets of Boolean functions. In this way, we identify easier cases, namely NP-complete, coNP-complete and polynomial cases. Thus, we get a detailed picture of the complexity of the propositional abduction problem, hence highlighting the sources of intractability. Further, we address the problem of counting the full explanations and prove a trichotomous classification theorem.
    Print ISSN: 0955-792X
    Electronic ISSN: 1465-363X
    Topics: Computer Science , Mathematics
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 82
    Publication Date: 2012-09-25
    Description: Epistemic logics with justification, S4LP and S4LPN , are combinations of the modal epistemic logic S4 and the Logic of Proofs LP , with some connecting principles. These logics together with the modal knowledge operator F ( F is known), contain infinitely many operators of the form t : F ( t is a justification for F ), where t is a term. Regarding the Realization Theorem of S4 , LP is the justification counterpart of S4 , in the sense that, every theorem of S4 can be transformed into a theorem of LP (by replacing all occurrences of by suitable terms), and vise versa. In this article, we first introduce a new cut-free sequent calculus $${\hbox{ LP }}_{L}^{\mathcal{G}}$$ for LP , and then extend it to obtain a cut-free sequent calculus for S4LP and a cut-free hypersequent calculus for S4LPN . All cut elimination theorems are proved syntactically. Moreover, these sequent systems enjoy a weak subformula property. Then, we show that theorems of S4LP can be realized in LP and theorems of S4LPN can be realized in JS5 (the justification counterpart of modal logic S5 ). Consequently, we prove that S4LP and S4LPN are conservative extensions of LP .
    Print ISSN: 0955-792X
    Electronic ISSN: 1465-363X
    Topics: Computer Science , Mathematics
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 83
    facet.materialart.
    Unknown
    Oxford University Press
    Publication Date: 2012-09-25
    Description: We solve unification problem for linear temporal logic ( $$\mathcal{L}$$ $$\mathcal{T}$$ $$\mathcal{L}$$ ). For any given formula , we verify if is unifiable in $$\mathcal{L}$$ $$\mathcal{T}$$ $$\mathcal{L}$$ ; if yes, we construct its unfolded form; and, next, by this form we directly write out the most general unifier for . Thus, we show any unifiable in $$\mathcal{L}$$ $$\mathcal{T}$$ $$\mathcal{L}$$ formula has a most general unifier (thus, $$\mathcal{L}$$ $$\mathcal{T}$$ $$\mathcal{L}$$ enjoys unitary unification), though we also show that there are unifiable in $$\mathcal{L}$$ $$\mathcal{T}$$ $$\mathcal{L}$$ formulas which are not projective.
    Print ISSN: 0955-792X
    Electronic ISSN: 1465-363X
    Topics: Computer Science , Mathematics
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 84
    Publication Date: 2012-09-25
    Description: In this article, we examine an argument-based semantics called semi-stable semantics . Semi-stable semantics is quite close to traditional stable semantics in the sense that every stable extension is also a semi-stable extension. One of the advantages of semi-stable semantics is that for finite argumentation frameworks there always exists at least one semi-stable extension. Furthermore, if there also exists at least one stable extension, then the semi-stable extensions coincide with the stable extensions. Semi-stable semantics can be seen as a general approach that can be applied to abstract argumentation, as well as to fields like default logic and answer set programming, yielding an interpretation with properties very similar to those of paraconsistent logic, including the properties of crash resistance and backward compatibility .
    Print ISSN: 0955-792X
    Electronic ISSN: 1465-363X
    Topics: Computer Science , Mathematics
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 85
    Publication Date: 2012-09-25
    Description: Trust is a mechanism for managing the uncertainty about autonomous entities and the information they store, and so can play an important role in any decentralized system. As a result, trust has been widely studied in multi-agent systems and related fields such as the semantic web. Here, we introduce a formal system of argumentation that can be used to reason using information about trust. This system is described as a set of graphs, which makes it possible to combine our approach with conventional representations of trust between individuals where the relationships between individuals are given in the form of a graph. The resulting system can easily relate the grounds of an argument to the agent that supplied the information, and can be used as the basis to compute Dungian notions of acceptability that take trust into account. We explore some of the properties of these argumentation graphs, examine the computation of trust and belief in the graphs and illustrate the capabilities of the system on an example from the trust literature.
    Print ISSN: 0955-792X
    Electronic ISSN: 1465-363X
    Topics: Computer Science , Mathematics
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 86
    Publication Date: 2012-09-25
    Description: Various logical formalisms with the freeze quantifier have been recently considered to model computer systems even though this is a powerful mechanism that often leads to undecidability. In this article, we study a linear-time temporal logic with past-time operators such that the freeze operator is only used to express that some value from an infinite set is repeated in the future or in the past. Such a restriction has been inspired by a recent work on spatio-temporal logics that suggests such a restricted use of the freeze operator. We show decidability of finitary and infinitary satisfiability by reduction into the verification of temporal properties in Petri nets by proposing a symbolic representation of models. This is a quite surprising result in view of the expressive power of the logic since the logic is closed under negation, contains future-time and past-time temporal operators and can express the nonce property and its negation. These ingredients are known to lead to undecidability with a more liberal use of the freeze quantifier. The article also contains developments about the relationships between temporal logics with the freeze operator and counter automata as well as reductions into first-order logics over data words.
    Print ISSN: 0955-792X
    Electronic ISSN: 1465-363X
    Topics: Computer Science , Mathematics
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 87
    Publication Date: 2012-09-25
    Description: In this article, some paraconsistent and temporal description logics are studied based on an embedding-based proof method. A new paraconsistent description logic, $$\mathcal{PALC}$$ , is obtained from the description logic $$\mathcal{ALC}$$ by adding a paraconsistent negation. Two temporal description logics, $$\mathcal{XALC}$$ and $$\mathcal{BALC}$$ l , are introduced by combining and modifying $$\mathcal{ALC}$$ and Prior’s tomorrow tense logic. $$\mathcal{XALC}$$ has the next-time operator, and $$\mathcal{BALC}$$ l has some restricted versions of the next-time, any-time and some-time operators, in which the time domain is bounded by a positive integer l . Some theorems for embedding $$\mathcal{PALC}$$ , $$\mathcal{XALC}$$ and $$\mathcal{BALC}$$ l into $$\mathcal{ALC}$$ are proved in a uniform way, and $$\mathcal{PALC}$$ , $$\mathcal{XALC}$$ and $$\mathcal{BALC}$$ l are shown to be decidable. Three tableau calculi for $$\mathcal{PALC}$$ , $$\mathcal{XALC}$$ and $$\mathcal{BALC}$$ l are introduced, and the completeness theorems for these calculi are proved.
    Print ISSN: 0955-792X
    Electronic ISSN: 1465-363X
    Topics: Computer Science , Mathematics
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 88
    Publication Date: 2012-09-25
    Print ISSN: 0955-792X
    Electronic ISSN: 1465-363X
    Topics: Computer Science , Mathematics
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 89
    Publication Date: 2016-01-30
    Description: We introduce a first sequent-style calculus for witnessed Gödel logic. Our calculus makes use of the cut rule. We show that this is inescapable by establishing a general result on the non-existence of suitable analytic calculi for a large class of first-order logics. These include witnessed Gödel logic, (fragments of) Łukasiewicz logic and intuitionistic logic extended with the quantifiers of classical logic.
    Print ISSN: 0955-792X
    Electronic ISSN: 1465-363X
    Topics: Computer Science , Mathematics
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 90
    facet.materialart.
    Unknown
    Oxford University Press
    Publication Date: 2016-01-30
    Description: The transition from a theory that turned out trivial to a consistent replacement need not proceed in terms of inconsistencies, which are negation gluts. Logics that tolerate gluts or gaps (or both) with respect to any logical symbol may serve as the lower limit for adaptive logics that assign a minimally abnormal consequence set to a given premise set. The same obtains for logics that tolerate a combination of kinds of gluts and gaps. This result runs counter to the obsession with inconsistency that classical logicians and paraconsistent logicians share. All such basic logics will be systematically reviewed; some variants will be outlined, and the claim will be argued for. While those logics tolerate gluts and gaps with respect to logical symbols, ambiguity logic tolerates ambiguities in non-logical symbols. Moreover, forms of tolerance may be combined, with zero logic as an extreme. In the baffling plethora of corrective adaptive logics (roads from trivial theories to consistent replacements), adaptive zero logic turns out theoretically interesting as well as practically useful. On the one hand all meaning becomes contingent, depending on the premise set. On the other hand, precisely adaptive zero logic provides one with an excellent analysing instrument. For example, it enables one to figure out which corrective adaptive logics lead, for a specific trivial theory, to a suitable and interesting minimally abnormal consequence set.
    Print ISSN: 0955-792X
    Electronic ISSN: 1465-363X
    Topics: Computer Science , Mathematics
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 91
    Publication Date: 2016-01-30
    Description: It is well-known that intuitionistic propositional logic Int may be faithfully embedded not just into the modal logic S4 but also into the provability logics GL and Grz of Gödel-Löb and Grzegorczyk, and also that there is a similar embedding of Grz into GL . Known proofs of these faithfulness results are short but model-theoretic and thus non-constructive. Here a labelled sequent system Grz for Grzegorczyk logic is presented and shown to be complete and therefore closed with respect to Cut . The completeness proof, being constructive, yields a constructive decision procedure, i.e. both a proof procedure for derivable sequents and a countermodel construction for underivable sequents. As an application, a constructive proof of the faithfulness of the embedding of Int into Grz and hence a constructive decision procedure for Int are obtained.
    Print ISSN: 0955-792X
    Electronic ISSN: 1465-363X
    Topics: Computer Science , Mathematics
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 92
    facet.materialart.
    Unknown
    Oxford University Press
    Publication Date: 2016-01-30
    Description: Hintikka's semantic game for classical logic is generalized to the family of all finite-valued matrices. This in turn serves as a springboard for developing game semantics for all propositional formulas with respect to arbitrary finite non-deterministic matrices. In this approach a new concept of non-deterministic valuation, called ‘liberal valuation’, emerges that augments the usually employed static and dynamic valuations in a natural manner. Liberal valuation is shown to correspond to unrestricted semantic games, while the characterization of static and dynamic valuations involves certain restrictions of the game that are handled by an interactive pruning procedure.
    Print ISSN: 0955-792X
    Electronic ISSN: 1465-363X
    Topics: Computer Science , Mathematics
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 93
    facet.materialart.
    Unknown
    Oxford University Press
    Publication Date: 2016-01-30
    Description: Justification logics refine modal logics by replacing the usual necessity operator with a family of justification terms that embody reasons for the necessity of a formula, rather than simply recording the fact of necessity. Many common modal logics have justification counterparts. The connection between a modal logic and its justification counterpart is through a Realization Theorem, which says that modal operators can be replaced in a precise way with justification terms so that modal theorems turn into justification logic theorems. In this article we present a new proof of Realization. We use the familiar machinery of consistency properties to prove a weak version, we call it Quasi-Realization. Then we show how to convert Quasi-Realizations into Realizations proper. Unlike most other treatments in the literature, the work here is not propositional, but first-order. Only one modal/justification logic is discussed, but the methods easily extend to other standard systems.
    Print ISSN: 0955-792X
    Electronic ISSN: 1465-363X
    Topics: Computer Science , Mathematics
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 94
    Publication Date: 2016-01-30
    Description: This article intends to contribute to the debate about the uses of paraconsistent reasoning in the foundations of set theory, by means of using the logics of formal inconsistency and by considering consistent and inconsistent sentences, as well as consistent and inconsistent sets. We establish the basis for new paraconsistent set-theories (such as ZFmbC and ZFCil ) under this perspective and establish their non-triviality, provided that ZF is consistent. By recalling how George Cantor himself, in his efforts towards founding set theory more than a century ago, not only used a form of ‘inconsistent sets’ in his mathematical reasoning, but regarded contradictions as beneficial, we argue that Cantor's handling of inconsistent collections can be related to ours.
    Print ISSN: 0955-792X
    Electronic ISSN: 1465-363X
    Topics: Computer Science , Mathematics
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 95
    facet.materialart.
    Unknown
    Oxford University Press
    Publication Date: 2016-01-30
    Description: Primal infon logic (PIL) was introduced in 2009 in the framework of policy and trust management. In the meantime, some generalizations appeared, and there have been some changes in the syntax of the basic PIL. This article is on the basic PIL, and one of our purposes is to ‘institutionalize’ the changes. We prove a small-model theorem for the propositional fragment of basic primal infon logic (PPIL), give a simple proof of the PPIL locality theorem and present a linear-time decision algorithm (announced earlier) for PPIL in a form convenient for generalizations. For the sake of completeness, we cover the universal fragment of basic PIL. We wish that this article becomes a standard reference on basic PIL.
    Print ISSN: 0955-792X
    Electronic ISSN: 1465-363X
    Topics: Computer Science , Mathematics
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 96
    Publication Date: 2016-01-30
    Description: In the context of non-monotonic reasoning different kinds of consequence relations are defined for reasoning from (possibly) inconsistent information. Examples are consequence relations that are characterized in terms of maximal consistent subsets of the premise set. The strong consequences are those formulas that follow by Classical Logic from every maximal consistent subset. The weak consequences follow from some maximal consistent subset. The free consequences follow from the set of formulas that belong to every maximal consistent subset. In this paper the question is discussed which of these consequence relations should be applied in which reasoning context. First the concerns that are expressed in the literature with respect to the usefulness of the weak consequences are addressed. Then it is argued that making weak inferences is sensible for some application contexts, provided one has a (dynamic) proof theory for the corresponding consequence relation. Such a dynamic proof theory is what adaptive logics offer. Finally, all this is illustrated by means of a very simple adaptive logic reconstruction of the free, strong, and weak consequences.
    Print ISSN: 0955-792X
    Electronic ISSN: 1465-363X
    Topics: Computer Science , Mathematics
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 97
    Publication Date: 2016-01-30
    Description: The LF $$\mathcal{P}$$ Framework is an extension of the Harper–Honsell–Plotkin's Edinburgh Logical Framework LF with external predicates , hence the name Open Logical Framework . This is accomplished by defining lock type constructors , which are a sort of -modality constructors , releasing their argument under the condition that a possibly external predicate is satisfied on an appropriate typed judgement. Lock types are defined using the standard pattern of constructive type theory, i . e . via introduction , elimination and equality rules . Using LF $$\mathcal{P}$$ , one can factor out the complexity of encoding specific features of logical systems, which would otherwise be awkwardly encoded in LF, e . g . side-conditions in the application of rules in Modal Logics, and sub-structural rules, as in non-commutative Linear Logic . The idea of LF $$\mathcal{P}$$ is that these conditions need only to be specified, while their verification can be delegated to an external proof engine, in the style of the Poincaré Principle or Deduction Modulo . Indeed such paradigms can be adequately formalized in LF $$\mathcal{P}$$ . We investigate and characterize the meta-theoretical properties of the calculus underpinning LF $$\mathcal{P}$$ : strong normalization, confluence and subject reduction. This latter property holds under the assumption that the predicates are well-behaved , i . e . closed under weakening, permutation , substitution and reduction in the arguments. Moreover, we provide a canonical presentation of LF $$\mathcal{P}$$ , based on a suitable extension of the notion of β - long normal form , allowing for smooth formulations of adequacy statements.
    Print ISSN: 0955-792X
    Electronic ISSN: 1465-363X
    Topics: Computer Science , Mathematics
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 98
    Publication Date: 2016-01-30
    Description: The ADC method of proof search in propositional natural deduction proposed in 2000 proceeds bottom up first by Analysing the sequent into sub-goals by applying all possible introduction rules, and then by checking whether each of these sub-goals can be established using only elimination rules ( Direct Chaining ). This looks simpler than the worst case complexity (PSPACE) of the derivability problem for intuitionistic propositional logic. We investigate the complexity of ADC for various fragments. ADC derivability is polynomially decidable for the &, -〉-fragment by a generalization of a familiar direct chaining algorithm for Horn formulas. Adding leads to a CoNP-complete fragment. A short counterexample in case the goal sequent is not ADC derivable is provided by witnessing all relevant disjunctions. Adding constant preserves CoNP completeness.
    Print ISSN: 0955-792X
    Electronic ISSN: 1465-363X
    Topics: Computer Science , Mathematics
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 99
    Publication Date: 2016-01-30
    Description: A kind of a bi-intuitionistic propositional logic is introduced that combines verification and its dual. This logic, 2Int , is motivated by a certain dualization of the natural deduction rules for intuitionistic propositional logic, Int . It is shown that 2Int can be faithfully embedded into Int with respect to validity. Moreover, 2Int can be faithfully embedded into dual intuitionistic logic, DualInt , with respect to a notion of dual validity. In 2Int , from a falsificationist perspective, intuitionistic negation internalizes support of truth, whereas from a verificationist perspective, co-negation internalizes support of falsity.
    Print ISSN: 0955-792X
    Electronic ISSN: 1465-363X
    Topics: Computer Science , Mathematics
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 100
    Publication Date: 2016-01-30
    Description: Nested sequent calculi are a useful generalization of ordinary sequent calculi, where sequents are allowed to occur within sequents. Nested sequent calculi have been profitably used in the area of (multi)-modal logic to obtain analytic and modular proof systems for these logics. In this work, we extend the realm of nested sequents by providing nested sequent calculi for the basic conditional logic CK and some of its significant extensions. We provide also a calculus for Kraus Lehman Magidor cumulative logic C. The calculi are internal (a sequent can be directly translated into a formula), cut-free and analytic. Moreover, they can be used to design (sometimes optimal) decision procedures for the respective logics, and to obtain complexity upper bounds. Our calculi are an argument in favour of nested sequent calculi for modal logics and alike, showing their versatility and power.
    Print ISSN: 0955-792X
    Electronic ISSN: 1465-363X
    Topics: Computer Science , Mathematics
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
Close ⊗
This website uses cookies and the analysis tool Matomo. More information can be found here...