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.
