More Like this

1. Founded semantics and constraint semantics of logic rules

   https://doi.org/10.1093/logcom/exaa056  

   Liu, Yanhong A; Stoller, Scott D (October 2020, Journal of Logic and Computation)

   null (Ed.)

   Abstract Logic rules and inference are fundamental in computer science and have been studied extensively. However, prior semantics of logic languages can have subtle implications and can disagree significantly, on even very simple programs, including in attempting to solve the well-known Russell’s paradox. These semantics are often non-intuitive and hard-to-understand when unrestricted negation is used in recursion. This paper describes a simple new semantics for logic rules, founded semantics, and its straightforward extension to another simple new semantics, constraint semantics, that unify the core of different prior semantics. The new semantics support unrestricted negation, as well as unrestricted existential and universal quantifications. They are uniquely expressive and intuitive by allowing assumptions about the predicates, rules and reasoning to be specified explicitly, as simple and precise binary choices. They are completely declarative and relate cleanly to prior semantics. In addition, founded semantics can be computed in linear time in the size of the ground program. 

   more » « less
2. Interval Signal Temporal Logic From Natural Inclusion Functions

   https://doi.org/10.1109/LCSYS.2023.3337744  

   Baird, Luke; Harapanahalli, Akash; Coogan, Samuel (January 2023, IEEE Control Systems Letters)

   We propose an interval extension of Signal Temporal Logic (STL) called Interval Signal Temporal Logic (I-STL). Given an STL formula, we consider an interval inclusion function for each of its predicates. Then, we use minimal inclusion functions for the min and max functions to recursively build an interval robustness that is a natural inclusion function for the robustness of the original STL formula. The resulting interval semantics accommodate, for example, uncertain signals modeled as a signal of intervals and uncertain predicates modeled with appropriate inclusion functions. In many cases, verification or synthesis algorithms developed for STL apply to I-STL with minimal theoretic and algorithmic changes, and existing code can be readily extended using interval arithmetic packages at negligible computational expense. To demonstrate I-STL, we present an example of offline monitoring from an uncertain signal trace obtained from a hardware experiment and an example of robust online control synthesis enforcing an STL formula with uncertain predicates. 

   more » « less
3. Integrating Logic Rules with Everything Else, Seamlessly

   https://doi.org/10.1017/S1471068423000108  

   LIU, YANHONG A; STOLLER, SCOTT D; TONG, YI; LIN, BO (July 2023, Theory and Practice of Logic Programming)

   This paper presents a language, Alda, that supports all of logic rules, sets, functions, updates, and objects as seamlessly integrated built-ins. The key idea is to support predicates in rules as set-valued variables that can be used and updated in any scope, and support queries using rules as either explicit or implicit automatic calls to an inference function. We have defined a formal semantics of the language, implemented a prototype compiler that builds on an object-oriented language that supports concurrent and distributed programming and on an efficient logic rule system, and successfully used the language and implementation on benchmarks and problems from a wide variety of application domains. We describe the compilation method and results of experimental evaluation. 

   more » « less
4. A Formalization of Core Why3 in Coq

   https://doi.org/10.1145/3632902  

   Cohen, Joshua_M; Johnson-Freyd, Philip (January 2024, Proceedings of the ACM on Programming Languages)

   Intermediate verification languages like Why3 and Boogie have made it much easier to build program verifiers, transforming the process into a logic compilation problem rather than a proof automation one. Why3 in particular implements a rich logic for program specification with polymorphism, algebraic data types, recursive functions and predicates, and inductive predicates; it translates this logic to over a dozen solvers and proof assistants. Accordingly, it serves as a backend for many tools, including Frama-C, EasyCrypt, and GNATProve for Ada SPARK. But how can we be sure that these tools are correct? The alternate foundational approach, taken by tools like VST and CakeML, provides strong guarantees by implementing the entire toolchain in a proof assistant, but these tools are harder to build and cannot directly take advantage of SMT solver automation. As a first step toward enabling automated tools with similar foundational guarantees, we give a formal semantics in Coq for the logic fragment of Why3. We show that our semantics are useful by giving a correct-by-construction natural deduction proof system for this logic, using this proof system to verify parts of Why3’s standard library, and proving sound two of Why3’s transformations used to convert terms and formulas into the simpler logics supported by the backend solvers. 

   more » « less
5. A new schema of logic representation and reasoning for automated building code compliance checking.

   Yang, F.; Zhang, J.; Chen, Y.; and Debs, L. (January 2022, Proceedings of the GPEA Polytechnic Summit 2022: Session Papers)

   Steinmetz, A. (Ed.)

   Manual building code compliance checking is a time-consuming, labor-intensive and error-prone process. Automated logic-based reasoning is an essential step in the automation of this process. There have been previous studies using logic programming languages for automated logic-based reasoning to support automated compliance checking (ACC) of building designs with building codes. As a high-performance implementation of the standard logic programming language, B-Prolog was widely used in these studies. However, due to the support of dynamic predicates and user-defined operators, the predicates’ functions vary according to different user definitions; therefore, B-Prolog is sometimes not reliable for building code reasoning. As a more expressive, scalable, and reliable alterative to B-Prolog, Picat, a logic-based multi-paradigm programming language, provides a new and potentially more powerful platform for automated logic-based reasoning in ACC. To explore the potential value of Picat in ACC, in this study, the authors compared Picat and B-Prolog performance in automatically checking 20 requirement rules in the 2015 International Building Code. The experimental results showed that the automated checking for building codes in the B-Prolog version was faster than that in the Picat version, whereas the Picat version was more reliable than the B-Prolog version. This could be the result of B-Prolog using unifica-tion and Picat using pattern matching for indexing rules. More potential applications of Picat in ACC domain need further research. Furthermore, this schema could be used in the teaching of ACC to graduate construction students, illustrating the need to focus on the reliability, predictability and scalability of the process, in order to provide a practical solution to improving code compliance checking processes. 

   more » « less