MRG home page - Research - Publications - Projects - Software - People

University of Edinburgh

Distributed Theorem proving/Proof Planning

With the increasing accessibility of multicore technologies and distributed computing networks, it has become imperative to investigate novel ways of using these concurrency and distribution technologies to tackle hard problems and to tap latent distribution and collaborative problem solving opportunities present in various tasks that computers are being used to solve.

Theorem proving, with its vast combinatorially explosive search spaces and increasingly complex and bigger problems, can benefit from these new ways of programming and new technologies. Also, such new approaches can open up fresh ways of thinking about the problem and the various algorithms used to tackle them.

This project investigates the application of novel concurrent/collaborative approaches as well as large scale data-parallelism appproaches to theorem proving tasks.

The hypothesis of the project is that this is possible, i.e, there is scope to do it and it is practically feasible to implement it and that there are gains to be made thereof in terms of speedup and higher success rate.

The hypothesis has been investigated by studying two disparate case studies: Propositional Satisfiability solver (SAT) and an LCF style tactic-based first order theorem prover and concurrency at both coarse and fine granularity levels have been considered. Prototypes for both the case studies have been developed in a functional programming language called Alice, an extension of Standard ML, with additional features for supporting concurrent, distributed programming. The prototypes are meant to be amenable for deployment on distributed environments like clusters.

These prototypes build on existing techniques by employing concurrent/distributed programming techniques. The SAT solver uses DPLL and Stalmarck algorithms in a co-operative manner. The first-order prover is a LCF-style sequent-calculus based prover and implements a suite of distributed tacticals employing well-known distributed programming abstractions/skeletals like producer-consumer, pipeline, and a novel abstraction called fastest-first, and message-passing techniques.

Future research directions include extending these techniques to proof planning. The proof planning systems available today are sequential systems. The paradigm of proof planning provides many latent opportunities that will benefit from the use of concurrent/distributed programming techniques. However, proof planners available today are largely sequential systems. A proof planner which allows for Incorporation of concurrent/distributed programming techniques will allow for tapping of these latent opportunities, thus enabling the engineering of a smarter, faster proof planner.

Here is a paper that describes the SAT work Concurrent-distributed programming techniques for SAT using DPLL-stålmarck

SriPriya G
Prof Alan Bundy
Dr Alan Smaill

Webpage maintained by: Sripriya.G     Webpage last updated: