Graph Algorithms for Improving Type-Logical Proof Search

TL;DR

This paper explores the application of graph algorithms to enhance type-logical proof search, introducing efficient methods for selecting optimal axiom links and top proof candidates to reduce search complexity.

Contribution

It presents novel polynomial-time algorithms for selecting optimal axiom links and top proof candidates in graph-based proof search, improving efficiency.

Findings

O(n^4) algorithm for optimal axiom link selection

O(kn^3) algorithm for top proof candidate selection

Reduced search space in type-logical proof search

Abstract

Proof nets are a graph theoretical representation of proofs in various fragments of type-logical grammar. In spite of this basis in graph theory, there has been relatively little attention to the use of graph theoretic algorithms for type-logical proof search. In this paper we will look at several ways in which standard graph theoretic algorithms can be used to restrict the search space. In particular, we will provide an O(n4) algorithm for selecting an optimal axiom link at any stage in the proof search as well as a O(kn3) algorithm for selecting the k best proof candidates.