Related papers: A two-level logic approach to reasoning about comp…
This thesis concerns the development of a framework that facilitates the design and analysis of formal systems. Specifically, this framework provides a specification language which supports the concise and direct description of formal…
Abella is an interactive system for reasoning about aspects of object languages that have been formally presented through recursive rules based on syntactic structure. Abella utilizes a two-level logic approach to specification and…
The approach to reasoning about structural operational semantics style specifications supported by the Abella system is discussed. This approach uses lambda tree syntax to treat object language binding and encodes binding related properties…
The logic of definitions is a family of logics for encoding and reasoning about judgments, which are atomic predicates specified by inference rules. A definition associates an atomic predicate with a logical formula, which may itself depend…
When reasoning about formal objects whose structures involve binding, it is often necessary to analyze expressions relative to a context that associates types, values, and other related attributes with variables that appear free in the…
The logic of hereditary Harrop formulas (HH) has proven useful for specifying a wide range of formal systems. This logic includes a form of hypothetical judgment that leads to dynamically changing sets of assumptions and that is key to…
Logic has proved essential for formally modeling software based systems. Such formal descriptions, frequently called specifications, have served not only as requirements documentation and formalisation, but also for providing the…
We present a logic named L_{LF} whose intended use is to formalize properties of specifications developed in the dependently typed lambda calculus LF. The logic is parameterized by the LF signature that constitutes the specification. Atomic…
The Abella interactive theorem prover has proven to be an effective vehicle for reasoning about relational specifications. However, the system has a limitation that arises from the fact that it is based on a simply typed logic:…
This thesis develops a framework for formalizing reasoning about specifications of systems written in LF. This formalization centers around the development of a reasoning logic that can express the sorts of properties which arise in…
Definite descriptions are expressions of the form "the unique $x$ satisfying property $C$," which allow reference to objects through their distinguishing characteristics. They play a crucial role in ontology and query languages, offering an…
The logic underlying the Abella proof assistant includes mechanisms for interpreting atomic predicates through fixed point definitions that can additionally be treated inductively or co-inductively. However, the original formulation of the…
We define a new decidable logic for expressing and checking invariants of programs that manipulate dynamically-allocated objects via pointers and destructive pointer updates. The main feature of this logic is the ability to limit the…
Many semantical aspects of programming languages, such as their operational semantics and their type assignment calculi, are specified by describing appropriate proof systems. Recent research has identified two proof-theoretic features that…
We describe the development of a logic for reasoning about specifications in the Edinburgh Logical Framework (LF). In this logic, typing judgments in LF serve as atomic formulas, and quantification is permitted over contexts and terms that…
Recursive relational specifications are commonly used to describe the computational structure of formal systems. Recent research in proof theory has identified two features that facilitate direct, logic-based reasoning about such…
Description logics are knowledge representation languages that have been designed to strike a balance between expressivity and computational tractability. Many different description logics have been developed, and numerous computational…
Several formal systems, such as resolution and minimal model semantics, provide a framework for logic programming. In this paper, we will survey the use of structural proof theory as an alternative foundation. Researchers have been using…
Structured reasoning over natural language inputs remains a core challenge in artificial intelligence, as it requires bridging the gap between unstructured linguistic expressions and formal logical representations. In this paper, we propose…
Combining higher-order abstract syntax and (co)induction in a logical framework is well known to be problematic. Previous work described the implementation of a tool called Hybrid, within Isabelle HOL, which aims to address many of these…