Bridge and Bound: A Logic-Based Framework for Abstracting (Preliminary Report)

TL;DR

Bridge and Bound introduces a logic-based framework for abstraction, called α-abstraction, built around a bridging theory that connects a source theory to an abstract vocabulary. Abstractions are represented as a pair of bounds (lower and upper) that respectively preserve entailment of sufficient conditions and necessary conditions, with the tightest abstraction given by the weakest sufficient and strongest necessary conditions derived from the bridging theory. The framework extends to first-order logic, leverages Ackermann-style second-order quantifier elimination, and analyzes the computational aspects of verification, tightest bounds, and exactness, including compositional properties for layered abstractions. The work provides formal foundations for systematic abstraction in AI and knowledge-based reasoning, and suggests practical avenues for applying the method to non-classical logics and scalable explanation/verification tasks.

Abstract

At its core, abstraction is the process of generalizing from specific instances to broader concepts or models, with the primary objective of reducing complexity while preserving properties essential to the intended purpose. It is a fundamental, often implicit, principle that structures the understanding, communication, and development of both scientific knowledge and everyday beliefs. Studies on abstraction have evolved from its origins in Ancient Greek philosophy through methodological approaches in psychological and philosophical theories to computational frameworks. Formally, abstraction can be understood as the transformation of a source representation into an abstract representation that discards certain details while retaining desirable features. In real-world modeling and reasoning, abstraction is crucial, particularly when managing imperfect or incomplete information that calls for approximate representations. This paper introduces a novel logic-based framework for modeling abstraction processes that goes beyond the traditional entailment of necessary conditions to encompass sufficient conditions as well. We define approximate abstractions, study their tightest and exact forms, and extend the approach to layered abstractions, enabling hierarchical simplification of complex systems and models. The computational complexity of the related reasoning tasks is also discussed. For clarity, our framework is developed within classical logic, chosen for its simplicity, expressiveness, and computational friendliness.

Figures (2)

• Figure 1: Approximate theory $\langle \mathcal{T}\xspace^l,\mathcal{T}\xspace^u\rangle$: any sufficient condition $C$ for $\mathcal{T}\xspace^l$ and any necessary condition $D$ of $\mathcal{T}\xspace^u$ is also a sufficient (respectively, necessary) condition of any theory located between bounds $\mathcal{T}\xspace^l$ and $\mathcal{T}\xspace^u$ (with respect to entailment). Arrows indicate implications.
• Figure 2: The role of theories in abstracting: $\mathcal{T}\xspace_S$ is a source theory, $\mathcal{T}\xspace_B$ is a bridging theory over vocabularies $\mathcal{V}\xspace_S$ and $\mathcal{V}\xspace_B$, respectively, $\mathcal{V}\xspace_A$ is an abstract vocabulary, and $\mathcal{T}\xspace^l,\mathcal{T}\xspace^u$ are a lower and an upper bound of an $\alpha$-abstraction. Dashed arrows represent implications.

Theorems & Definitions (22)

• Lemma 2.1: Lemma 3.1 in dlssnc
• Lemma 2.2
• Definition 3.1: Approximate abstraction
• Proposition 3.2
• Example 3.3
• Definition 3.4: Tightest abstraction
• Theorem 3.5
• Example 3.6: Example \ref{['ex:game-mood']} continued
• Proposition 3.7
• Definition 3.8: Exact abstraction