Searcharxiv⌕ Search

arXiv subjects

Yanhong A. Liu

Publications and source records attributed to Yanhong A. Liu.

At least 19 recordsLinked to original sources
arXiv2026

Specifying Paxos for System Builders: Pseudocode Made Executable

This paper presents a precise executable specification---as a faithful mapping from the pseudocode---of Paxos for System Builders, a practical protocol for replication and consensus in distributed systems. Paxos for System Builders has both a robust implementation in C and a clean pseudocode for critical protocol details. This paper shows how the protocol pseudocode can be expressed easily, essentially line-by-line, in a precise high-level language, DistAlgo, for direct execution in distributed systems. Precise specification and direct execution help significantly in understanding the protocol logic and in automatically checking, tracing, and visualizing protocol runs. They also led to discoveries and fixes of small, difficult-to-catch omissions and liveness bugs in the pseudocode though not the C code. The resulting program also has acceptable performance while having similar size as the pseudocode.

cs.DC↗
arXiv2026

Integrating Reasoning Systems for Trustworthy AI, Proceedings of the 4th Workshop on Logic and Practice of Programming (LPOP)

This proceedings contains abstracts and position papers for the work to be presented at the fourth Logic and Practice of Programming (LPOP) Workshop. The workshop is to be held in Dallas, Texas, USA, and as a hybrid event, on October 13, 2024, in conjunction with the 40th International Conference on Logic Programming (ICLP). The focus of this workshop is integrating reasoning systems for trustworthy AI, especially including integrating diverse models of programming with rules and constraints.

cs.AI↗
arXiv2026

Efficiency of Analysis of Transitive Relations using Query-Driven, Ground-and-Solve, and Fact-Driven Inference

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.

cs.DB↗
arXiv2025

Incremental Computation: What Is the Essence?

Incremental computation aims to compute more efficiently on changed input by reusing previously computed results. We give a high-level overview of works on incremental computation, and highlight the essence underlying all of them, which we call incrementalization -- the discrete counterpart of differentiation in calculus. We present the gist of a systematic method for incrementalization, and a systematic method centered around it -- called Iterate-Incrementalize-Implement -- for program design and optimization, as well as algorithm design and optimization. We illustrate the methods with example applications in arithmetic computations, recursive functions, graph analysis, and distributed algorithms. At a meta-level, with historical contexts and for future directions, we stress the power of high-level data, control, and module abstractions in developing new and better algorithms and programs as well as their precise complexities.

cs.PL↗
arXiv2025

Resilience through Automated Adaptive Configuration for Distribution and Replication

This paper presents a powerful automated framework for making complex systems resilient under failures, by optimized adaptive distribution and replication of interdependent software components across heterogeneous hardware components with widely varying capabilities. A configuration specifies how software is distributed and replicated: which software components to run on each computer, which software components to replicate, which replication protocols to use, etc. We present an algorithm that, given a system model and resilience requirements, (1) determines initial configurations of the system that are resilient, and (2) generates a reconfiguration policy that determines reconfiguration actions to execute in response to failures and recoveries. This model-finding algorithm is based on state-space exploration and incorporates powerful optimizations, including a quotient reduction based on a novel equivalence relation between states. We present experimental results from successfully applying a prototype implementation of our framework to a model of an autonomous driving system.

cs.DC↗
arXiv2025

Logical Lease Litigation: Prolog and LLMs for Rental Law Compliance in New York

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.

cs.AI↗
arXiv2025

LP-LM: No Hallucinations in Question Answering with Logic Programming

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.

cs.AI↗
arXiv2023

Benchmarking for Integrating Logic Rules with Everything Else

Integrating logic rules with other language features is increasingly sought after for advanced applications that require knowledge-base capabilities. To address this demand, increasingly more languages and extensions for such integration have been developed. How to evaluate such languages? This paper describes a set of programming and performance benchmarks for evaluating languages supporting integrated use of rules and other features, and the results of evaluating such an integrated language together with logic languages and languages not supporting logic rules.

cs.PL↗
arXiv2023

Integrating Logic Rules with Everything Else, Seamlessly

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.

cs.PL↗
arXiv2023

Specification and Runtime Checking of Derecho, A Protocol for Fast Replication for Cloud Services

Reliable distributed systems require replication and consensus among distributed processes to tolerate process and communication failures. Understanding and assuring the correctness of protocols for replication and consensus have been a significant challenge. This paper describes the precise specification and runtime checking of Derecho, a more recent, sophisticated protocol for fast replication and consensus for cloud services. A precise specification must fill in missing details and resolve ambiguities in English and pseudocode algorithm descriptions while also faithfully following the descriptions. To help check the correctness of the protocol, we also performed careful manual analysis and increasingly systematic runtime checking. We obtain a complete specification that is directly executable, and we discover and fix a number of issues in the pseudocode. These results were facilitated by the already detailed pseudocode of Derecho and made possible by using DistAlgo, a language that allows distributed algorithms to be easily and clearly expressed and directly executed.

cs.DC↗
arXiv2022

Proceedings of the 2nd Workshop on Logic and Practice of Programming (LPOP)

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.

cs.PL↗
arXiv2022

Recursive Rules with Aggregation: A Simple Unified Semantics

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.

cs.DB↗
arXiv2022

Programming with rules and everything else, seamlessly

Logic rules are powerful for expressing complex reasoning and analysis problems. At the same time, they are inconvenient or impossible to use for many other aspects of applications. Integrating rules in a language with sets and functions, and furthermore with updates to objects, has been a subject of significant study. What's lacking is a language that integrates all constructs seamlessly. This paper presents a language, Alda, that supports all of rules, sets, functions, updates, and objects as seamlessly integrated built-ins, including concurrent and distributed processes. The key idea is to support predicates as set-valued variables that can be used and updated in any scope, and support queries and inference with both explicit and automatic calls to an inference function. We develop a complete formal semantics for Alda. We design a compilation framework that ensures the declarative semantics of rules, while also being able to exploit available optimizations. We describe a prototype implementation that builds on a powerful extension of Python and employs an efficient logic rule engine. We develop a range of benchmarks and present results of experiments to demonstrate Alda's power for programming and generally good performance.

cs.PL↗
arXiv2020

Assurance of Distributed Algorithms and Systems: Runtime Checking of Safety and Liveness

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.

cs.SE↗
arXiv2020

Knowledge of Uncertain Worlds: Programming with Logical Constraints

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.

cs.LO↗
arXiv2020

Discrete Math with Programming: A Principled Approach

Discrete mathematics is the foundation of computer science. It focuses on concepts and reasoning methods that are studied using math notations. It has long been argued that discrete math is better taught with programming, which takes concepts and computing methods and turns them into executable programs. What has been lacking is a principled approach that supports all central concepts of discrete math -- especially predicate logic -- and that directly and precisely connects math notations with executable programs. This paper introduces such an approach. It is based on the use of a powerful language that extends the Python programming language with proper logic quantification ("for all" and "exists some"), as well as declarative set comprehension (also known as set builder) and aggregation (e.g., sum and product). Math and logical statements can be expressed precisely at a high level and be executed directly on a computer, encouraging declarative programming together with algorithmic programming. We describe the approach, detailed examples, experience in using it, and the lessons learned.

cs.CY↗
arXiv2020

LPOP: Challenges and Advances in Logic and Practice of Programming

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.

cs.PL↗