More Like this

1. An Answer Set Programming Framework for Reasoning about Agents' Beliefs and Truthfulness of Statements

   https://doi.org/10.24963/kr.2020/8  

   Balduccini, Marcello; Gelfond, Michael; Pontelli, Enrico; Son, Tran Cao (July 2020, Proceedings of the 17th International Conference on Principles of Knowledge Representation and Reasoning)

   null (Ed.)

   The paper proposes a framework for capturing how an agent’s beliefs evolve over time in response to observations and for answering the question of whether statements made by a third party can be believed. The basic components of the framework are a formalism for reasoning about actions, changes, and observations and a formalism for default reasoning. The paper describes a concrete implementation that leverages answer set programming for determining the evolution of an agent's ``belief state'', based on observations, knowledge about the effects of actions, and a theory about how these influence an agent's beliefs. The beliefs are then used to assess whether statements made by a third party can be accepted as truthful. The paper investigates an application of the proposed framework in the detection of man-in-the-middle attacks targeting computers and cyber-physical systems. Finally, we briefly discuss related work and possible extensions. 

   more » « less
2. QED: A Powerful Query Equivalence Decider for SQL

   https://doi.org/10.14778/3681954.3682024  

   Wang, Shuxian; Pan, Sicheng; Cheung, Alvin (July 2024, Proceedings of the VLDB Endowment)

   Checking query equivalence is of great significance in database systems. Prior work in automated query equivalence checking sets the first steps in formally modeling and reasoning about query optimization rules, but only supports a limited number of query features. In this paper, we present Qed, a new framework for query equivalence checking based on bag semantics. Qed uses a new formalism called Q-expressions that models queries using different normal forms for efficient equivalence checking, and models features such as integrity constraints and NULLs in a principled way unlike prior work. Our formalism also allows us to define a new query fragment that encompasses many real-world queries with a complete equivalence checking algorithm, assuming a complete first-order theory solver. Empirically, Qed can verify 299 out of 444 query pairs extracted from the Calcite framework and 979 out of 1287 query pairs extracted from CockroachDB, which is more than 2× the number of cases proven by prior state-of-the-art solver. 

   more » « less
3. Semantic Fluency in Design Reasoning

   Quintana-Cifuentes, Jenny; Purzer, Senay (December 2022, International journal of engineering education)

   During design, different forms of reasoning shape the designers’ decision-making. As a result, the ability to fluently transition across various forms of reasoning is essential. The purpose of this study is two-fold: first is to introduce and explain the concept of Semantic Fluency in Design Reasoning, as the ability to transition across multiple forms of reasoning fluently. To identify these transitions, this study used the Design Reasoning Quadrants framework, which represents four quadrants: experiential observations (reasoning based on observations and experiences), trade-offs (reasoning recognizing multiple competing design requirements), first-principles (reasoning requiring disciplinary understandings), and complex abstractions (reasoning in envisioning new situations). The second purpose of this study is to illustrate semantic fluency in a design review conversation. We selected and presented three different forms of transitions identified through our analysis of conversations between students and design reviewers. Our analysis revealed evidence of semantic fluency in young designers. Mike, one of the students, demonstrated fluency across three quadrants (experiential observations, trade-offs, and first-principles). Lisa and David demonstrated two-quadrant transitions. Lisa had fluency from experiential observations to trade-offs, and David transitioned from experiential observations to first-principles. We recommend the intentional use of design reviews to elicit student reasoning in design and adopt questioning strategies to promote fluency across different forms of design reasoning. 

   more » « less
4. Argosy: verifying layered storage systems with recovery refinement

   https://doi.org/10.1145/3314221.3314585  

   Chajed, Tej; Tassarotti, Joseph; Kaashoek, M. Frans; Zeldovich, Nickolai (June 2019, Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI ’19))

   Reasoning about storage systems is challenging because these systems make persistence guarantees even if the system crashes at any point. To achieve these crash-safety guarantees, storage systems include recovery procedures to restore the system to a consistent state after a crash. Moreover, large-scale systems are structured as multiple stacked layers and can require recovery at multiple layers of abstraction. Formal verification can ensure that crash-safety guarantees hold regardless of when the system crashes. To make verification tractable, large-scale systems should be verified in a modular fashion, layer-by-layer in the software stack. Layered recovery makes modularity challenging because the system can crash in the middle of a high-level recovery procedure and must start over from the low-level recovery procedure. We present Argosy, a framework for machine-checked proofs of storage systems that supports layered recovery implementations with modular proofs. The framework is based on combinators for transition relations that are inspired by Kleene algebra, which provides a convenient formalism for specifying and reasoning about crashes and recovery. On top of this framework, we implement Crash Hoare Logic (CHL), the program logic used by FSCQ. Using the logic, we have verified an example of layered recovery featuring a write-ahead log on top of a disk, which itself runs by replicating over two unreliable disks. The metatheory of the framework, the soundness of the program logic, and these examples are all verified in the Coq theorem prover. 

   more » « less
5. A revised energy formalism for common-envelope evolution: repercussions for planetary engulfment and the formation of neutron star binaries

   Yarza, Ricardo; Everson, Rosa Wallace; Ramirez-Ruiz, Enrico (September 2022, ArXivorg)

   Common-envelope evolution is a stage in binary system evolution in which a giant star engulfs a companion. The standard energy formalism is an analytical framework to estimate the amount of energy transferred from the companion's shrinking orbit into the envelope of the star that engulfed it. We show analytically that this energy transfer is larger than predicted by the standard formalism. As the orbit of the companion shrinks, the mass it encloses becomes smaller, and the companion is less bound than if the enclosed mass had remained constant. Therefore, more energy must be transferred to the envelope for the orbit to shrink further. We derive a revised energy formalism that accounts for this effect, and discuss its consequences in two contexts: the formation of neutron star binaries, and the engulfment of planets and brown dwarfs by their host stars. The companion mass required to eject the stellar envelope is smaller by up to 50% , leading to differences in common-envelope evolution outcomes. The energy deposition in the outer envelope of the star, which is related to the transient luminosity and duration, is up to a factor of ≈7 higher. Common-envelope efficiency values above unity, as defined in the literature, are thus not necessarily unphysical, and result at least partly from an incomplete description of the energy deposition. The revised energy formalism presented here can improve our understanding of stellar merger and common-envelope observations and simulations. 

   more » « less