More Like this

1. The Nonexistence of Unicorns and Many-Sorted Löwenheim–Skolem Theorems

   https://doi.org/10.1007/978-3-031-71162-6_34  

   Przybocki, Benjamin; Toledo, Guilherme; Zohar, Yoni; Barrett, Clark (September 2024, Springer Nature Switzerland)

   Platzer, André; Rozier, Kristin Yvonne; Pradella, Matteo; Rossi, Matteo (Ed.)

   Abstract Stable infiniteness, strong finite witnessability, and smoothness are model-theoretic properties relevant to theory combination in satisfiability modulo theories. Theories that are strongly finitely witnessable and smooth are calledstrongly politeand can be effectively combined with other theories. Toledo, Zohar, and Barrett conjectured that stably infinite and strongly finitely witnessable theories are smooth and therefore strongly polite. They called counterexamples to this conjectureunicorn theories, as their existence seemed unlikely. We prove that, indeed, unicorns do not exist. We also prove versions of the Löwenheim–Skolem theorem and the Łoś–Vaught test for many-sorted logic. 

   more » « less
2. Combining Stable Infiniteness and (Strong) Politeness

   https://doi.org/10.1007/s10817-023-09684-0  

   Sheng, Ying; Zohar, Yoni; Ringeissen, Christophe; Reynolds, Andrew; Barrett, Clark; Tinelli, Cesare (December 2023, Journal of Automated Reasoning)

   Polite theory combination is a method for obtaining a solver for a combination of two (or more) theories using the solvers of each individual theory as black boxes. Unlike the earlier Nelson–Oppen method, which is usable only when both theories are stably infinite, only one of the theories needs to be strongly polite in order to use the polite combination method. In its original presentation, politeness was required from one of the theories rather than strong politeness, which was later proven to be insufficient. The first contribution of this paper is a proof that indeed these two notions are different, obtained by presenting a polite theory that is not strongly polite. We also study several variants of this question. The cost of the generality afforded by the polite combination method, compared to the Nelson–Oppen method, is a larger space of arrangements to consider, involving variables that are not necessarily shared between the purified parts of the input formula. The second contribution of this paper is a hybrid method (building on both polite and Nelson–Oppen combination), which aims to reduce the number of considered variables when a theory is stably infinite with respect to some of its sorts but not all of them. The time required to reason about arrangements is exponential in the worst case, so reducing the number of variables considered has the potential to improve performance significantly. We show preliminary evidence for this by demonstrating significant speed-up on a smart contract verification benchmark. 

   more » « less
3. Combining Finite Combination Properties: Finite Models and Busy Beavers

   https://doi.org/10.1007/978-3-031-43369-6_9  

   Toledo, Guilherme V.; Zohar, Yoni; Barrett, Clark (September 2023, Lecture Notes in Computer Science)

   Sattler, Uli; Suda, Martin (Ed.)

   This work is a part of an ongoing effort to understand the relationships between properties used in theory combination. We here focus on including two properties that are related to shiny theories: the finite model property and stable finiteness. For any combination of properties, we consider the question of whether there exists a theory that exhibits it. When there is, we provide an example with the simplest possible signature. One particular class of interest includes theories with the finite model property that are not finitely witnessable. To construct such theories, we utilize the Busy Beaver function. 

   more » « less
4. Dempster-Shafer Theoretic Learning of Indirect Speech Act Comprehension Norms

   Wen, Ruchen; Siddiqui, Mohammed Aun; Williams, Tom (February 2020, Proceedings of the AAAI Conference on Artificial Intelligence)

   For robots to successfully operate as members of human-robot teams, it is crucial for robots to correctly understand the intentions of their human teammates. This task is particularly difficult due to human sociocultural norms: for reasons of social courtesy (e.g., politeness), people rarely express their intentions directly, instead typically employing polite utterance forms such as Indirect Speech Acts (ISAs). It is thus critical for robots to be capable of inferring the intentions behind their teammates’ utterances based on both their interaction context (including, e.g., social roles) and their knowledge of the sociocultural norms that are applicable within that context. This work builds off of previous research on understanding and generation of ISAs using Dempster-Shafer Theoretic Uncertain Logic, by showing how other recent work in Dempster-Shafer Theoretic rule learning can be used to learn appropriate uncertainty intervals for robots’ representations of sociocultural politeness norms. 

   more » « less
5. Fresh Start: Encouraging Politeness in Wakeword-Driven Human-Robot Interaction

   https://doi.org/10.1145/3568162.3576959  

   Wen, Ruchen; Hanson, Alyssa; Han, Zhao; Williams, Tom (March 2023, ACM/IEEE International Conference on Human-Robot Interaction)

   Deployed social robots are increasingly relying on wakeword-based interaction, where interactions are human-initiated by a wakeword like “Hey Jibo”. While wakewords help to increase speech recognition accuracy and ensure privacy, there is concern that wakeword-driven interaction could encourage impolite behavior because wakeword-driven speech is typically phrased as commands. To address these concerns, companies have sought to use wake- word design to encourage interactant politeness, through wakewords like “⟨Name⟩, please”. But while this solution is intended to encourage people to use more “polite words”, researchers have found that these wakeword designs actually decrease interactant politeness in text-based communication, and that other wakeword designs could better encourage politeness by priming users to use Indirect Speech Acts. Yet there has been no previous research to directly compare these wakewords designs in in-person, voice-based human-robot interaction experiments, and previous in-person HRI studies could not effectively study carryover of wakeword-driven politeness and impoliteness into human-human interactions. In this work, we conceptually reproduced these previous studies (n=69) to assess how the wakewords “Hey ⟨Name⟩”, “Excuse me ⟨Name⟩”, and “⟨Name⟩, please” impact robot-directed and human-directed politeness. Our results demonstrate the ways that different types of linguistic priming interact in nuanced ways to induce different types of robot-directed and human-directed politeness. 

   more » « less