Yanhong A. Liu

Yanhong A. Liu, John Idogun, Scott D. Stoller et al.

Logic rules allow analysis of complex relationships to be expressed easily, especially for transitive relations in critical applications. However, understanding and predicting the efficiency of different inference methods remain challenging, even for simplest rules given different kinds of input data. This paper analyzes the efficiency of all three types of well-known inference methods -- query-driven, ground-and-solve, and fact-driven -- along with their respective optimizations, and compares with optimal complexities for the first time, for analyzing transitive graph relations. We also experiment with rule systems widely considered to have the best performance. We analyze all well-known rule variants and widely varying input graphs. The results include precisely calculated optimal time complexities; comparative analysis across different inference methods, rule variants, and graph types; confirmation with performance experiments; as well as discovery of a performance bug.

David S. Warren, Peter Van Roy, Yanhong A. Liu

This proceedings contains abstracts and position papers for the work presented at the second Logic and Practice of Programming (LPOP) Workshop. The workshop was held online, virtually in place of Chicago, USA, on November 15, 2010, in conjunction with the ACM SIGPLAN Conference on Systems, Programming, Languages, and Applications: Software for Humanity (SPLASH) 2020. The purpose of this workshop is to be a bridge between different areas of computer science that use logic as a practical tool. We take advantage of the common language of formal logic to exchange ideas between these different areas.

Katherine Wu, Yanhong A. Liu

Large language models (LLMs) are able to generate human-like responses to user queries. However, LLMs exhibit inherent limitations, especially because they hallucinate. This paper introduces LP-LM, a system that grounds answers to questions in known facts contained in a knowledge base (KB), facilitated through semantic parsing in Prolog, and always produces answers that are reliable. LP-LM generates a most probable constituency parse tree along with a corresponding Prolog term for an input question via Prolog definite clause grammar (DCG) parsing. The term is then executed against a KB of natural language sentences also represented as Prolog terms for question answering. By leveraging DCG and tabling, LP-LM runs in linear time in the size of input sentences for sufficiently many grammar rules. Performing experiments comparing LP-LM with current well-known LLMs in accuracy, we show that LLMs hallucinate on even simple questions, unlike LP-LM.

Sanskar Sehgal, Yanhong A. Liu

Legal cases require careful logical reasoning following the laws, whereas interactions with non-technical users must be in natural language. As an application combining logical reasoning using Prolog and natural language processing using large language models (LLMs), this paper presents a novel approach and system, LogicLease, to automate the analysis of landlord-tenant legal cases in the state of New York. LogicLease determines compliance with relevant legal requirements by analyzing case descriptions and citing all relevant laws. It leverages LLMs for information extraction and Prolog for legal reasoning. By separating information extraction from legal reasoning, LogicLease achieves greater transparency and control over the legal logic applied to each case. We evaluate the accuracy, efficiency, and robustness of LogicLease through a series of tests, achieving 100% accuracy and an average processing time of 2.57 seconds. LogicLease presents advantages over state-of-the-art LLM-based legal analysis systems by providing clear, step-by-step reasoning, citing specific laws, and distinguishing itself by its ability to avoid hallucinations -- a common issue in LLMs.

Yanhong A. Liu, Scott D. Stoller

This paper presents a general framework and methods for complete programming and checking of distributed algorithms at a high-level, as in pseudocode languages, but precisely specified and directly executable, as in formal specification languages and practical programming languages, respectively. The checking framework, as well as the writing of distributed algorithms and specification of their safety and liveness properties, use DistAlgo, a high-level language for distributed algorithms. We give a complete executable specification of the checking framework, with a complete example algorithm and example safety and liveness properties.

David S. Warren, Yanhong A. Liu

This article describes the work presented at the first Logic and Practice of Programming (LPOP) Workshop, which was held in Oxford, UK, on July 18, 2018, in conjunction with the Federated Logic Conference (FLoC) 2018. Its focus is challenges and advances in logic and practice of programming. The workshop was organized around a challenge problem that specifies issues in role-based access control (RBAC), with many participants proposing combined imperative and declarative solutions expressed in the languages of their choice.

Yanhong A. Liu, Scott D. Stoller

Complex reasoning problems are most clearly and easily specified using logical rules, but require recursive rules with aggregation such as count and sum for practical applications. Unfortunately, the meaning of such rules has been a significant challenge, leading to many disagreeing semantics. This paper describes a unified semantics for recursive rules with aggregation, extending the unified founded semantics and constraint semantics for recursive rules with negation. The key idea is to support simple expression of the different assumptions underlying different semantics, and orthogonally interpret aggregation operations using their simple usual meaning. We present a formal definition of the semantics, prove important properties of the semantics, and compare with prior semantics. In particular, we present an efficient inference over aggregation that gives precise answers to all examples we have studied from the literature. We also apply our semantics to a wide range of challenging examples, and show that our semantics is simple and matches the desired results in all cases. Finally, we describe experiments on the most challenging examples, exhibiting unexpectedly superior performance over well-known systems when they can compute correct answers.

Yanhong A. Liu, Scott D. Stoller

Programming with logic for sophisticated applications must deal with recursion and negation, which together have created significant challenges in logic, leading to many different, conflicting semantics of rules. This paper describes a unified language, DA logic, for design and analysis logic, based on the unifying founded semantics and constraint semantics, that support the power and ease of programming with different intended semantics. The key idea is to provide meta-constraints, supports the use of uncertain information in the form of either undefined values or possible combinations of values or both, and promote the use of knowledge units that can be instantiated by any new predicates, including predicates with additional arguments.

K. Tuncay Tekle, Yanhong A. Liu

Given a set of Datalog rules, facts, and a query, answers to the query can be inferred bottom-up starting from the facts or top-down starting from the query. For efficiency, top-down evaluation is extended with memoization of inferred facts, and bottom-up evaluation is performed after transformations to make rules driven by the demand from the query. Prior work has shown their precise complexity analysis and relationships. However, when Datalog is extended with even stratified negation, which has a simple and universally accepted semantics, transformations to make rules demand-driven may result in non-stratified negation, which has had many complex semantics and evaluation methods. This paper presents (1) a simple extension to demand transformation, a transformation to make rules demand-driven for Datalog without negation, to support stratified negation, and (2) a simple extension to an optimal bottom-up evaluation method for Datalog with stratified negation, to handle non-stratified negation in the resulting rules. We show that the method provides precise complexity guarantees. It is also optimal in that only facts needed for top-down evaluation of the query are inferred and each firing of a rule to infer such a fact takes worst-case constant time. We extend the precise relationship between top-down evaluation and demand-driven bottom-up evaluation to Datalog with stratified negation. Finally, we show experimental results for performance, as well as applications to previously challenging examples.

Scott D. Stoller, Yanhong A. Liu

Diversity can significantly increase the resilience of systems, by reducing the prevalence of shared vulnerabilities and making vulnerabilities harder to exploit. Work on software diversity for security typically creates variants of a program using low-level code transformations. This paper is the first to study algorithm diversity for resilience. We first describe how a method based on high-level invariants and systematic incrementalization can be used to create algorithm variants. Executing multiple variants in parallel and comparing their outputs provides greater resilience than executing one variant. To prevent different parallel schedules from causing variants' behaviors to diverge, we present a synchronized execution algorithm for DistAlgo, an extension of Python for high-level, precise, executable specifications of distributed algorithms. We propose static and dynamic metrics for measuring diversity. An experimental evaluation of algorithm diversity combined with implementation-level diversity for several sequential algorithms and distributed algorithms shows the benefits of algorithm diversity.

Christopher Kane, Bo Lin, Saksham Chand et al.

The interfaces exposed by commonly used cryptographic libraries are clumsy, complicated, and assume an understanding of cryptographic algorithms. The challenge is to design high-level abstractions that require minimum knowledge and effort to use while also allowing maximum control when needed. This paper proposes such high-level abstractions consisting of simple cryptographic primitives and full declarative configuration. These abstractions can be implemented on top of any cryptographic library in any language. We have implemented these abstractions in Python, and used them to write a wide variety of well-known security protocols, including Signal, Kerberos, and TLS. We show that programs using our abstractions are much smaller and easier to write than using low-level libraries, where size of security protocols implemented is reduced by about a third on average. We show our implementation incurs a small overhead, less than 5 microseconds for shared key operations and less than 341 microseconds (< 1%) for public key operations. We also show our abstractions are safe against main types of cryptographic misuse reported in the literature.

Yanhong A. Liu

This article presents an overview of applications of logic programming, classifying them based on the abstractions and implementations of logic languages that support the applications. The three key abstractions are join, recursion, and constraint. Their essential implementations are for-loops, fixed points, and backtracking, respectively. The corresponding kinds of applications are database queries, inductive analysis, and combinatorial search, respectively. We also discuss language extensions and programming paradigms, summarize example application problems by application areas, and touch on example systems that support variants of the abstractions with different implementations.

David S. Warren, Yanhong A. Liu

This document describes the contributions of the 2016 Applications of Logic Programming Workshop (AppLP), which was held on October 17 and associated with the International Conference on Logic Programming (ICLP) in Flushing, New York City.

Yanhong A. Liu, Scott D. Stoller

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.

Yanhong A. Liu, Jon Brandvein, Scott D. Stoller et al.

Object queries are essential in information seeking and decision making in vast areas of applications. However, a query may involve complex conditions on objects and sets, which can be arbitrarily nested and aliased. The objects and sets involved as well as the demand---the given parameter values of interest---can change arbitrarily. How to implement object queries efficiently under all possible updates, and furthermore to provide complexity guarantees? This paper describes an automatic method. The method allows powerful queries to be written completely declaratively. It transforms demand as well as all objects and sets into relations. Most importantly, it defines invariants for not only the query results, but also all auxiliary values about the objects and sets involved, including those for propagating demand, and incrementally maintains all of them. Implementation and experiments with problems from a variety of application areas, including distributed algorithms and probabilistic queries, confirm the analyzed complexities, trade-offs, and significant improvements over prior work.