Abstract: We propose a formal language that allows for transposing biological information precisely and rigorously into machine-readable information. This language, which we call Zsyntax, is grounded on a particular type of non-classical logic, and it can be used to write algorithms and computer programs. We present it as a first step towards a comprehensive formal language for molecular biology in which any biological process can be written and analyzed as a sort of logical ââdeductionââ. Moreover, we illustrate the potential value of this language, both in the field of text mining and in that of biological prediction.
Abstract: In this paper we investigate the problem of measuring social mobility when the social status of individuals is given by their rank. In order to sensibly represent the rank mobility of subgroups within a given society, we address the problem in terms of partial permutation matrices which include standard (âglobalâ) matrices as a special case. We first provide a characterization of a partial ordering on partial matrices which, in the standard case of global matrices, coincides with the well-known âconcordanceâ ordering. We then provide a characterization of an index of rank mobility based on partial matrices and show that, in the standard case of comparing global matrices, it is equivalent to Spearman's Ï index.
Abstract: In this paper, we provide an application-oriented characterization of a class of distance functions monotonically related to the Euclidean distance in terms of some general properties of distance functions between real-valued vectors. Our analysis hinges upon two fundamental properties of distance functions that we call âvalue-sensitivityâ and âorder-sensitivityâ. We show how these two general properties, combined with natural monotonicity considerations, lead to characterization results that single out several versions of Euclidean distance from the wide class of separable distance functions. We then discuss and motivate our results in two different and apparently unrelated application areasâmobility measurement and spatial voting theoryâand propose our characterization as a test for deciding whether Euclidean distance (or some suitable variant) should be used in your favourite application context.
Abstract: Deductive inference is usually regarded as being âtautologicalâ or âana-
lyticalâ: the information conveyed by the conclusion is contained in the information
conveyed by the premises. This idea, however, clashes with the undecidability of ï¬rst-
order logic and with the (likely) intractability of Boolean logic. In this article, we
address the problem both from the semantic and the proof-theoretical point of view
and propose a hierarchy of propositional logics that are all tractable (i.e. decidable
in polynomial time), although by means of growing computational resources, and
converge towards classical propositional logic. The underlying claim is that this hi-
erarchy can be used to represent increasing levels of âdepthâ or âinformativenessâ of
Boolean reasoning. Special attention is paid to the most basic logic in this hierarchy,
the pure âintelim logicâ, which satisï¬es all the requirements of a natural deduction
system (allowing both introduction and elimination rules for each logical operator)
while admitting of a feasible (quadratic) decision procedure. We argue that this logic
is âanalyticâ in a particularly strict sense, in that it rules out any use of âvirtual
informationâ, which is chieï¬y responsible for the combinatorial explosion of standard
classical systems. As a result, analyticity and tractability are reconciled and growing
degrees of computational complexity are associated with the depth at which the use
of virtual information is allowed.
Abstract: In this paper we explore a generalization of traditional abduction which can simultaneously perform two different tasks: (i) given an unprovable sequent G, find a sentence H such that , H G is provable (hypothesis generation); (ii) given a provable sequent G, find a sentence H such that H and the proof of , H G is simpler than the proof of G (lemma generation). We argue that the two tasks should not be distinguished, and present a general procedure for finding suitable hypotheses or lemmas. When the original sequent is provable, the abduced formula can be seen as a cut formula with respect to Gentzen's sequent calculus, so the abduction method is cut-based. Our method is based on the tableau-like system KE and we argue for its advantages over existing abduction methods based on traditional Smullyan-style Tableaux.
Abstract: We investigate the semantics of the logical systems obtained by introducing the modalities and into the family of substructural implication logics (including relevant, linear and intuitionistic implication). Then, in the spirit of the LDS (Labelled Deductive Systems) methodology, we "import" this semantics into the classical proof system KE. This leads to the formulation of a uniform labelled refutation system for the new logics which is a natural extension of a system for substructural implication developed by the first two authors in a previous paper.
Abstract: The method of analytic tableaux is a direct descendant of Gentzenâs cut-free sequent calculus and is regarded as a paradigm of the notion of analytic deduction in classical logic. However, cut-free systems are anomalous from the proof-theoretical, the semantical and the computational point of view. Firstly, they cannot represent the use of auxiliary lemmas in proofs. Secondly, they cannot express the bivalence of classical logic. Thirdly, they are extremely inefficient, as is emphasized by the âÂÂcomputational scandalâ that such systems cannot potynomially simulate the truth-tables. None of these anomalies occurs if the cut rule is allowed. This raises the problem of formulating a proof system which incorporates a cut rule and yet can provide a suitable model of classical analytic deduction. For this purpose we present an alternative refutation system for classical logic, that we call KE. This system, though being "close"  to Smullyanâs tableau method, is not cut-free but includes a classical cut rule which is not eliminable. Analytic deductions are then obtained by restricting the cut rule to analytic applications, namely applications that do not violate the subformula principle. It turns out that this analytic restriction of the KE system shares all the interesting properties of Smullyanâs tableau method and of cut-free systemsâÂÂit obeys the subformula principle and admits systematic refutation proceduresâÂÂbut uniformly and essentially improves on them from the complexity viewpoint. In particular, we show that the analytic KE system linearly simulates the tableau method, but the tableau method cannot p-simulate the analytic KE system. Finally, we show that every proof system that can simulate the cut rule in a constant number of steps is strictly more powerful than cut-free systems, from the complexity viewpoint, even in the domain of analytic deduction. Hence, the speed-up of the analytic KE system does not depend on the form of the operational rules but only on the analytic cut rule.
Abstract: In this series of papers we set out to generalize the notion of classical analytic deduction (i.e., deduction via elimination rules) by combining the methodology of labelled deductive systems (LDS) with the classical systemKE. LDS is a unifying framework for the study of logics and of their interactions. In the LDS approach the basic units of logical derivation are not just formulae butlabelled formulae, where the labels belong to a given labelling algebra. The derivation rules act on the labels as well as on the formulae, according to certain fixed rules of propagation. By virtue of the extra power of the labelling algebras, standard (classical or intuitionistic) proof systems can be extended to cover a much wider territory without modifying their structure. The systemKE is a new tree method for classical analytic deduction based on analytic cut.KE is a refutation system, like analytic tableaux and resolution, but it is essentially more efficient than tableaux and, unlike resolution, does not require any reduction to normal form. We start our investigation with the family of substructural logics. These are logical systems (such as Lambekâs calculus, Anderson and Belnapâs relevance logic, and Girardâs linear logic) which arise from disallowing some or all of the usual structural properties of the notion of logical consequence. This extension of traditional logic yields a subtle analysis of the logical operators which is more in tune with the needs of applications. In this paper we generalize the classicalKE system via the LDS methodology to provide a uniform refutation system for the family of substructural logics. The main features of this generalized method are the following: (a) each logic in the family is associated with a labelling algebra; (b) the tree-expansion rules (for labelled formulae) are the same for all the logics in the family; (c) the difference between one logic and the other is captured by the conditions under which a branch is declared closed; (d) such conditions depend only on the labelling algebra associated with each logic; and (e) classical and intuitionistic negations are characterized uniformly, by means of the same tree-expansion rules, and their difference is reduced to a difference in the labelling algebra used in closing a branch. In this first part we lay the theoretical foundations of our method. In the second part we shall continue our investigation of substructural logics and discuss the algorithmic aspects of our approach.
Abstract: We show that Smullyanâs analytic tableaux cannot p-simulate the truth-tables. We identify the cause of this computational breakdown and relate it to an underlying semantic difficulty which is common to the whole tradition originating in Gentzenâs sequent calculus, namely the dissonance between cut-free proofs and the Principle of Bivalence. Finally we discuss some ways in which this principle can be built into a tableau-like method without affecting its "analytic" nature.
Abstract: In this paper we set out to make a contribution towards the solution of the logical omniscience problem. We maintain that the problem can be properly solved by restricting the classical notion of logical consequence rather than by waiving closure of the propositional attitudes under logical consequence. We suggest that an interesting alternative solution could be based on Depth-Bounded Boolean Logics, a novel incremental approach to the characterization of classical propositional logic that construes it as the limit of an infinite sequence of weaker tractable logics. Agents committed to these logics can be seen as approximations to the idealized reasoning agent of standard epistemic, doxastic and information logic. The full decision problem for each of the approximating logics is solvable in polynomial time - although its complexity grows as we proceed along the approximation sequence -ÂÂ with no restriction to any particular syntactic fragment. Moreover, the meaning of the logical operators is the same for all logics and is explained in purely informational terms -ÂÂ that is, in terms of informational interpretations of "true"Â and "ÂÂfalse"ÂÂ -ÂÂ in such a way that the most basic inference principles of classical propositional logic, including disjunctive syllogism, are preserved throughout the sequence.
Abstract: De Finetti suggested that scoring rules -ÂÂ namely, loss functions by which a forecaster is virtually charged depending on the degree of inaccuracy of his predictions - could be employed also to provide a compelling argument for probabilism. However, De Finetti'ÂÂs choice of a specifiÂc scoring rule for this purpose (Brier'ÂÂs quadratic rule) appears somewhat arbitrary, and the general pragmatic flavour of the argument -Â which makes it a variant of the well-known "Dutch Book Theorem"ÂÂ ÂÂ has been deemed unsuitable for an epistemic justification of probabilism. In this paper we suggest how Brier'ÂÂs rule may be justified on epistemic grounds by means of a strategy that is diffÂerent from the one usually adopted for this purpose, taking advantage of a recent characterization result concerning distance functions between real-valued vectors.
