skip to main content
US FlagAn official website of the United States government
dot gov icon
Official websites use .gov
A .gov website belongs to an official government organization in the United States.
https lock icon
Secure .gov websites use HTTPS
A lock ( lock ) or https:// means you've safely connected to the .gov website. Share sensitive information only on official, secure websites.

Explore Research Products in the PAR
It may take a few hours for recently added research products to appear in PAR search results.


Title: A (mostly) symbolic system for monotonic inference with unscoped Episodic Logical Forms
We implement the formalization of natural logic-like monotonic inference using Unscoped Episodic Logical Forms (ULFs) by Kim et al. (2020). We demonstrate this system’s capacity to handle a variety of challenging semantic phenomena using the FraCaS dataset (Cooper et al., 1996).These results give empirical evidence for prior claims that ULF is an appropriate representation to mediate natural logic-like inferences.  more » « less
Award ID(s):
1940981
PAR ID:
10299972
Author(s) / Creator(s):
Date Published:
Journal Name:
NAtural LOgic Meets MAchine Learning (NALOMA'21)
Format(s):
Medium: X
Sponsoring Org:
National Science Foundation
More Like this
  1. ; ; ; (, Schloss Dagstuhl – Leibniz-Zentrum für Informatik)
    Endrullis, Jörg; Schmitz, Sylvain (Ed.)
    Graded modal logics generalise standard modal logics via families of modalities indexed by an algebraic structure whose operations mediate between the different modalities. The graded "of-course" modality !_r captures how many times a proposition is used and has an analogous interpretation to the of-course modality from linear logic; the of-course modality from linear logic can be modelled by a linear exponential comonad and graded of-course can be modelled by a graded linear exponential comonad. Benton showed in his seminal paper on Linear/Non-Linear logic that the of-course modality can be split into two modalities connecting intuitionistic logic with linear logic, forming a symmetric monoidal adjunction. Later, Fujii et al. demonstrated that every graded comonad can be decomposed into an adjunction and a "strict action". We give a similar result to Benton, leveraging Fujii et al.’s decomposition, showing that graded modalities can be split into two modalities connecting a graded logic with a graded linear logic. We propose a sequent calculus, its proof theory and categorical model, and a natural deduction system which we show is isomorphic to the sequent calculus system. Interestingly, our system can also be understood as Linear/Non-Linear logic composed with an action that adds the grading, further illuminating the shared principles between linear logic and a class of graded modal logics. 
    more » « less
  2. ; ; ; (, Biological Conservation)
    Many African large carnivore populations are declining due to decline of the herbivore populations on which they depend. We recently noted that the densities of true apex carnivores like the lion and spotted hyena correlate strongly with prey density, but competitively subordinate carnivores like the African wild dog benefit from competitive release when density of apex carnivores is low, so the expected effect of a simultaneous decrease in resources and dominant competitors is not obvious. We found that when prey density drops below a tipping point, the relationship of wild dog density to prey density changes sign, and wild dog density declines. We also noted that ‘prey depletion provides a mechanistically direct explanation of patterns in wild dog dynamics that have been attributed to climate change’ (Creel et al., 2023). Woodroffe et al. concur that prey depletion is an important threat, but suggest that we fail to understand the logic of their assertion that “climate change is likely to cause population collapse” (Rabaiotti et al., 2022), because the “identification of climate change as a threat is not based upon observed temporal trends in wild dog demography”. This statement misses our fundamental point. The data that Woodroffe et al. analyzed were collected over a period with rising temperatures and declining prey populations, so whether or not one tests for a time trend in demography, the data themselves are affected by two patterns: 
    more » « less
  3. ; ; ; ; ; (, ACM Conference on Computer and Communications Security (CCS))
    Symbolic methods have been used extensively for proving security of cryptographic protocols in the Dolev-Yao model, and more recently for proving security of cryptographic primitives and constructions in the computational model. However, existing methods for proving security of cryptographic constructions in the computational model often require significant expertise and interaction, or are fairly limitedin scope and expressivity. This paper introduces a symbolic approach for proving security of cryptographic constructions based on the Learning With Errors assumption (Regev, STOC 2005). Such constructions are instances of lattice-based cryptography and are extremely important due to their potential role in post-quantum cryptography. Following (Barthe, Gregoire and Schmidt, CCS 2015), our approach combines a computational logic and deducibility problems—a standard tool for representing the adversary’s knowledge, the Dolev-Yao model. The computational logic is used to capture (indistinguishability-based) security notions and drive the security proofs whereas deducibility problems are used as side-conditions to control that rules of the logic are applied correctly. We then use AutoLWE, an implementation of the logic, to deliver very short or even automatic proofs of several emblematic constructions, including CPAPKE (Gentry et al., STOC 2008), (Hierarchical) Identity-Based Encryption (Agrawal et al. Eurocrypt 2010), Inner Product Encryption (Agrawal et al. Asiacrypt 2011), CCA-PKE (Micciancio et al., Eurocrypt 2012). The main technical novelty beyond AutoLWE is a set of (semi-)decision procedures for deducibility problems, using extensions of Grobner basis computations for subalgebras in the non-commutative setting (instead of ideals in the commutative setting). Our procedures cover the theory of matrices, which is required for lattice-based assumption, as well as the theory of non-commutative rings, fields, and Diffie-Hellman exponentiation, in its standard, bilinear and multilinear forms. Additionally, AutoLWE supports oracle-relative assumptions, which are used specifically to apply (advanced forms of) the Leftover Hash Lemma, an information-theoretical tool widely used in lattice-based proofs. 
    more » « less
  4. ; ; ; ; ; (, ACM Conf. on Computer and Communications Security)
    Symbolic methods have been used extensively for proving security of cryptographic protocols in the Dolev-Yao model, and more recently for proving security of cryptographic primitives and constructions in the computational model. However, existing methods for proving security of cryptographic constructions in the computational model often require significant expertise and interaction, or are fairly limited in scope and expressivity. This paper introduces a symbolic approach for proving security of cryptographic constructions based on the Learning With Errors assumption (Regev, STOC 2005). Such constructions are instances of lattice-based cryptography and are extremely important due to their potential role in post-quantum cryptography. Following (Barthe, Gre ́goire and Schmidt, CCS 2015), our approach combines a computational logic and deducibility problems—a standard tool for representing the adversary’s knowledge, the Dolev-Yao model. The computational logic is used to capture (indistinguishability-based) security notions and drive the security proofs whereas deducibility problems are used as side-conditions to control that rules of the logic are applied correctly. We then use AutoLWE, an implementation of the logic, to deliver very short or even automatic proofs of several emblematic constructions, including CPA- PKE (Gentry et al., STOC 2008), (Hierarchical) Identity-Based Encryption (Agrawal et al. Eurocrypt 2010), Inner Product Encryption (Agrawal et al. Asiacrypt 2011), CCA-PKE (Micciancio et al., Eurocrypt 2012). The main technical novelty beyond AutoLWE is a set of (semi-)decision procedures for deducibility problems, using extensions of Grobner basis computations for subalgebras in the (non-)commutative setting (instead of ideals in the commutative setting). Our procedures cover the theory of matrices, which is required for lattice-based assumption, as well as the theory of non-commutative rings, fields, and Diffie-Hellman exponentiation, in its standard, bilinear and multilinear forms. Additionally, AutoLWE supports oracle-relative assumptions, which are used specifically to apply (advanced forms of) the Leftover Hash Lemma, an information-theoretical tool widely used in lattice-based proofs. 
    more » « less
  5. ; ; ; (, Journal of Mathematical Logic)
    We address the question of consistency strength of certain filters and ultrafilters which fail to satisfy the Galvin property. We answer questions [Benhamou and Gitik, Ann. Pure Appl. Logic 173 (2022) 103107; Questions 7.8, 7.9], [Benhamou et al., J. Lond. Math. Soc. 108(1) (2023) 190–237; Question 5] and improve theorem [Benhamou et al., J. Lond. Math. Soc. 108(1) (2023) 190–237; Theorem 2.3]. 
    more » « less
  • Citation Formats
  • MLA
  • APA
  • Chicago
  • BibTeX
  • Save / Share this Record
  • Send to Email