scholarly journals Density of truth in modal logics

2006 ◽  
Vol DMTCS Proceedings vol. AG,... (Proceedings) ◽  
Author(s):  
Zofia Kostrzycka
Keyword(s):  
Binary Tree ◽  
Modal Logics ◽  
Propositional Variable ◽  
Modal Formula ◽  
International Audience

International audience The aim of this paper is counting the probability that a random modal formula is a tautology. We examine $\{ \to,\Box \}$ fragment of two modal logics $\mathbf{S5}$ and $\mathbf{S4}$ over the language with one propositional variable. Any modal formula written in such a language may be interpreted as a unary binary tree. As it is known, there are finitely many different formulas written in one variable in the logic $\mathbf{S5}$ and this is the key to count the proportion of tautologies of $\mathbf{S5}$ among all formulas. Although the logic $\mathbf{S4}$ does not have this property, there exist its normal extensions having finitely many non-equivalent formulas.

scholarly journals On density of truth of the intuitionistic logic in one variable

2008 ◽  
Vol DMTCS Proceedings vol. AI,... (Proceedings) ◽  
Author(s):  
Zofia Kostrzycka
Keyword(s):  
Intuitionistic Logic ◽  
Classical Logic ◽  
Propositional Logic ◽  
Propositional Variable ◽  
Intuitionistic Propositional Logic ◽  
International Audience

International audience In this paper we focus on the intuitionistic propositional logic with one propositional variable. More precisely we consider the standard fragment $\{ \to ,\vee ,\bot \}$ of this logic and compute the proportion of tautologies among all formulas. It turns out that this proportion is different from the analog one in the classical logic case.

scholarly journals Dual filtered graphs

2015 ◽  
Vol DMTCS Proceedings, 27th... (Proceedings) ◽  
Author(s):  
Rebecca Patrias ◽  
Pavlo Pylyavskyy
Keyword(s):  
Hopf Algebra ◽  
Binary Tree ◽  
International Audience ◽  
Dual Graded Graphs ◽  
Young’S Lattice

International audience We define a $K$ -theoretic analogue of Fomin’s dual graded graphs, which we call dual filtered graphs. The key formula in the definition is $DU - UD = D + I$. Our major examples are $K$ -theoretic analogues of Young’s lattice, the binary tree, and the graph determined by the Poirier-Reutenauer Hopf algebra. Most of our examples arise via two constructions, which we call the Pieri construction and the Möbius construction. The Pieri construction is closely related to the construction of dual graded graphs from a graded Hopf algebra, as described in Bergeron-Lam-Li, Nzeutchap, and Lam-Shimozono. The Möbius construction is more mysterious but also potentially more important, as it corresponds to natural insertion algorithms. Nous définissons un analogue $K$ -théorique aux graphes gradués en dualité de Fomin que nous appelons les graphes filtrés en dualité. La formule importante pour la définition est $DU - UD = D + I$. Nos principaux exemples sont un analogue $K$ -théorique aux graphe de Young, l’arbre binaire, et un graphe déterminé par l’algèbre de Hopf de Poirier-Reutenauer. La plupart de nos exemples surviennent de deux constructions que nous appelons la construction de Pieri et la construction de Möbius. La construction de Pieri est étroitement liée à la construction des graphes gradués en dualité d’une algèbre graduée de Hopf à la Bergeron-Lam-Li, Nzeutchap, et Lam-Shimozono. La construction de Möbius est plus mystérieuse, mais aussi peut-être plus importante car cette construction correspond aux algorithmes d’insertion naturelles.

scholarly journals The height of the Lyndon tree

2013 ◽  
Vol DMTCS Proceedings vol. AS,... (Proceedings) ◽  
Author(s):  
Lucas Mercier ◽  
Philippe Chassaing
Keyword(s):  
Binary Tree ◽  
Large Deviation ◽  
Random Variables ◽  
Convergence In Probability ◽  
Eulerian Numbers ◽  
Deviation Rate ◽  
Rate Functions ◽  
International Audience ◽  
Lyndon Words

International audience We consider the set $\mathcal{L}_n<$ of n-letters long Lyndon words on the alphabet $\mathcal{A}=\{0,1\}$. For a random uniform element ${L_n}$ of the set $\mathcal{L}_n$, the binary tree $\mathfrak{L} (L_n)$ obtained by successive standard factorization of $L_n$ and of the factors produced by these factorization is the $\textit{Lyndon tree}$ of $L_n$. We prove that the height $H_n$ of $\mathfrak{L} (L_n)$ satisfies $\lim \limits_n \frac{H_n}{\mathsf{ln}n}=\Delta$, in which the constant $\Delta$ is solution of an equation involving large deviation rate functions related to the asymptotics of Eulerian numbers ($\Delta ≃5.092\dots $). The convergence is the convergence in probability of random variables.

scholarly journals Modal logics with hard diamond-free fragments

2020 ◽  
Vol 30 (1) ◽  
pp. 3-25
Author(s):  
Antonis Achilleos
Keyword(s):  
General Setting ◽  
Modal Logics ◽  
Propositional Variable ◽  
High Complexity

Abstract We investigate the complexity of modal satisfiability for a family of multi-modal logics with interdependencies among the modalities. In particular, we examine four characteristic multi-modal logics with dependencies and demonstrate that, even if we restrict the formulae to be diamond-free and to have only one propositional variable, these logics still have a high complexity. This result identifies and isolates two sources of complexity: the presence of axiom $D$ for some of the modalities and certain modal interdependencies. We then further investigate and characterize the complexity of the diamond-free, 1-variable fragments of multi-modal logics in a general setting.

Proof-search and countermodel generation for non-normal modal logics: The theorem prover PRONOM

2021 ◽  
Vol 14 (2) ◽  
pp. 215-229
Author(s):  
Tiziano Dalmonte ◽  
Sara Negri ◽  
Nicola Olivetti ◽  
Gian Luca Pozzato
Keyword(s):  
Modal Logics ◽  
Experimental Results ◽  
Theorem Prover ◽  
Basic System ◽  
Sequent Calculi ◽  
Modal Formula ◽  
Left Hand ◽  
Proof Search ◽  
The Right ◽  
Normal Modal Logics

In this work we present PRONOM, a theorem prover and countermodel generator for non-normal modal logics. PRONOM implements some labelled sequent calculi recently introduced for the basic system E and its extensions with axioms M, N, and C based on bi-neighbourhood semantics. PRONOM is inspired by the methodology of leanTAP and is implemented in Prolog. When a modal formula is valid, then PRONOM computes a proof (a closed tree) in the labelled calculi having a sequent with an empty left-hand side and containing only that formula on the right-hand side as a root, otherwise PRONOM is able to extract a model falsifying it from an open, saturated branch. The paper shows some experimental results, witnessing that the performances of PRONOM are promising.

scholarly journals Descendants and ascendants in binary trees

1997 ◽  
Vol Vol. 1 ◽  
Author(s):  
Alois Panholzer ◽  
Helmut Prodinger
Keyword(s):  
Generating Functions ◽  
Binary Tree ◽  
Binary Trees ◽  
Zeilberger’S Algorithm ◽  
International Audience ◽  
Explicit Formulae ◽  
Zeilberger's Algorithm

International audience There are three classical algorithms to visit all the nodes of a binary tree - preorder, inorder and postorder traversal. From this one gets a natural labelling of the n internal nodes of a binary tree by the numbers 1, 2, ..., n, indicating the sequence in which the nodes are visited. For given n (size of the tree) and j (a number between 1 and n), we consider the statistics number of ascendants of node j and number of descendants of node j. By appropriate trivariate generating functions, we are able to find explicit formulae for the expectation and the variance in all instances. The heavy computations that are necessary are facilitated by MAPLE and Zeilberger's algorithm. A similar problem comes fromlabelling the leaves from left to right by 1, 2, ..., n and considering the statistic number of ascendants (=height) of leaf j. For this, Kirschenhofer [1] has computed the average. With our approach, we are also able to get the variance. In the last section, a table with asymptotic equivalents is provided for the reader's convenience.

scholarly journals Disjunctive Normal Form for Multi-Agent Modal Logics Based on Logical Separability

2019 ◽  
Vol 33 ◽  
pp. 2817-2826
Author(s):  
Liangda Fang ◽  
Kewen Wang ◽  
Zhe Wang ◽  
Ximing Wen
Keyword(s):  
Normal Form ◽  
Propositional Logic ◽  
Disjunctive Normal Form ◽  
Modal Logics ◽  
Multi Agent Systems ◽  
Modal Formula ◽  
Agent Systems ◽  
Multi Agent ◽  
Automatic Planning ◽  
Reasoning Tasks

Modal logics are primary formalisms for multi-agent systems but major reasoning tasks in such logics are intractable, which impedes applications of multi-agent modal logics such as automatic planning. One technique of tackling the intractability is to identify a fragment called a normal form of multiagent logics such that it is expressive but tractable for reasoning tasks such as entailment checking, bounded conjunction transformation and forgetting. For instance, DNF of propositional logic is tractable for these reasoning tasks. In this paper, we first introduce a notion of logical separability and then define a novel disjunctive normal form SDNF for the multiagent logic Kn, which overcomes some shortcomings of existing approaches. In particular, we show that every modal formula in Kn can be equivalently casted as a formula in SDNF, major reasoning tasks tractable in propositional DNF are also tractable in SDNF, and moreover, formulas in SDNF enjoy the property of logical separability. To demonstrate the usefulness of our approach, we apply SDNF in multi-agent epistemic planning. Finally, we extend these results to three more complex multi-agent logics Dn, K45n and KD45n.

scholarly journals An extension of Tamari lattices

2015 ◽  
Vol DMTCS Proceedings, 27th... (Proceedings) ◽  
Author(s):  
Louis-François Préville-Ratelle ◽  
Xavier Viennot
Keyword(s):  
Symmetric Group ◽  
Binary Tree ◽  
Prime Numbers ◽  
Binary Trees ◽  
Square Lattice ◽  
Reverse Order ◽  
Tamari Lattice ◽  
Nous Montrons ◽  
International Audience ◽  
Tamari Lattices

International audience For any finite path $v$ on the square lattice consisting of north and east unit steps, we construct a poset Tam$(v)$ that consists of all the paths lying weakly above $v$ with the same endpoints as $v$. For particular choices of $v$, we recover the traditional Tamari lattice and the $m$-Tamari lattice. In particular this solves the problem of extending the $m$-Tamari lattice to any pair $(a; b)$ of relatively prime numbers in the context of the so-called rational Catalan combinatorics.For that purpose we introduce the notion of canopy of a binary tree and explicit a bijection between pairs $(u; v)$ of paths in Tam$(v)$ and binary trees with canopy $v$. Let $(\overleftarrow{v})$ be the path obtained from $v$ by reading the unit steps of $v$ in reverse order and exchanging east and north steps. We show that the poset Tam$(v)$ is isomorphic to the dual of the poset Tam$(\overleftarrow{v})$ and that Tam$(v)$ is isomorphic to the set of binary trees having the canopy $v$, which is an interval of the ordinary Tamari lattice. Thus the usual Tamari lattice is partitioned into (smaller) lattices Tam$(v)$, where the $v$’s are all the paths of length $n-1$ on the square lattice.We explain possible connections between the poset Tam$(v)$ and (the combinatorics of) the generalized diagonal coinvariant spaces of the symmetric group. Pour tout chemin $v$ sur le réseau carré formé de pas Nord et Est, nous construisons un ensemble partiellement ordonné Tam $(v)$ dont les éléments sont les chemins au dessus de $v$ et ayant les mêmes extrémités. Pour certains choix de $v$ nous retrouvons le classique treillis de Tamari ainsi que son extension $m$-Tamari. En particulier nous résolvons le problème d’étendre le treillis $m$-Tamari à toute paire $(a; b)$ d’entiers premiers entre eux dans le contexte de la combinatoire rationnelle de Catalan.Pour ceci nous introduisons la notion de canopée d’un arbre binaire et explicitons une bijection entre les paires $(u; v)$ de chemins dans Tam$(v)$ et les arbres binaires ayant la canopée $v$. Soit $(\overleftarrow{v})$ le chemin obtenu en lisant les pas en ordre inverse et en échangeant les pas Est et Nord. Nous montrons que Tam$(v)$ est isomorphe au dual de Tam$(\overleftarrow{v})$ et que Tam$(v)$ est isomorphe à l’ensemble des arbres binaires ayant la canopée $v$, qui est un intervalle du treillis de Tamari ordinaire. Ainsi le traditionnel treillis de Tamari admet une partition en plus petits treillis Tam$(v)$, où les $v$ sont tous les chemins de longueur $n-1$ sur le réseau carré. Enfin nous explicitons les liens possibles entre l’ensemble ordonné Tam$(v)$ et (la combinatoire des) espaces diagonaux coinvariants généralisés du groupe symétrique.

scholarly journals Noncommutative symmetric functions with matrix parameters

2012 ◽  
Vol DMTCS Proceedings vol. AR,... (Proceedings) ◽  
Author(s):  
Alain Lascoux ◽  
Jean-Christophe Novelli ◽  
Jean-Yves Thibon
Keyword(s):  
Binary Tree ◽  
Symmetric Functions ◽  
Noncommutative Symmetric Functions ◽  
International Audience

International audience We define new families of noncommutative symmetric functions and quasi-symmetric functions depending on two matrices of parameters, and more generally on parameters associated with paths in a binary tree. Appropriate specializations of both matrices then give back the two-vector families of Hivert, Lascoux, and Thibon and the noncommutative Macdonald functions of Bergeron and Zabrocki. Nous définissons de nouvelles familles de fonctions symétriques non-commutatives et de fonctions quasi-symétriques, dépendant de deux matrices de paramètres, et plus généralement, de paramètres associés à des chemins dans un arbre binaire. Pour des spécialisations appropriées, on retrouve les familles à deux vecteurs de Hivert-Lascoux-Thibon et les fonctions de Macdonald non-commutatives de Bergeron-Zabrocki.

scholarly journals Left and right length of paths in binary trees or on a question of Knuth

2006 ◽  
Vol DMTCS Proceedings vol. AG,... (Proceedings) ◽  
Author(s):  
Alois Panholzer
Keyword(s):  
Binary Tree ◽  
Limiting Distribution ◽  
Binary Trees ◽  
Tree Model ◽  
Random Size ◽  
International Audience ◽  
Left And Right ◽  
The Common ◽  
The Difference ◽  
The Right

International audience We consider extended binary trees and study the common right and left depth of leaf $j$, where the leaves are labelled from left to right by $0, 1, \ldots, n$, and the common right and left external pathlength of binary trees of size $n$. Under the random tree model, i.e., the Catalan model, we characterize the common limiting distribution of the suitably scaled left depth and the difference between the right and the left depth of leaf $j$ in a random size-$n$ binary tree when $j \sim \rho n$ with $0< \rho < 1$, as well as the common limiting distribution of the suitably scaled left external pathlength and the difference between the right and the left external pathlength of a random size-$n$ binary tree.

Sign in / Sign up

Export Citation Format

Share Document