Presentation and activity reports

The PROTHEO project's goal is to conceive and realize tools for specifying and verifying software. To achieve this goal, we work on an environment that allows the prototyping of such tools, on demonstration tools specialized in recurrence proofs or in some educational theories, and on proof techniques that focus on using constraints and rewriting rules.

The project is based on three research themes: constraints solving, mecanising rules and strategies based deduction, and automatic theorems demonstration.

Rewriting and strategies

Keywords : rewriting, strategies, rewrite based programming, functional programming

Rewriting is one of the main themes of the project being considered and studied in order to model computation (in case of confluent and terminating rewrite systems) or deduction in which case non specific requirements are needed. Rewrite rules could be used to define the notions of a relation, a logic or a calculus. Strategies guiding the application of rewrite rules have been studied since a long time and appear to be central in the definition of efficient evaluation tools as well as in the definition of deduction processes. The rewriting calculus gives us the general framework on which to found our works on this topic.

Constraints

Keywords : constraint solving, satisfiability, combination problem

The study of the satisfiability and the solving of constraint systems on term or on specific domains is central in computation and in deduction. Combination techniques are of fundamental use to decompose the problem. The cooperation of constraint solvers or reasoners could also be used to break down the difficulty of solving large problems.

Automated Deduction

Keywords : déduction, réécriture, récurrence, contrainte, paramodulation, résolution

The combination of constraint solving and rewriting techniques is present in many if not all systems of automated deduction. The study of their consistent combination and the design of complete and efficient theorem provers based on them leads to the possibility to check program properties in a more systematic way. For example Noetherian rewrite systems allow to perform inductive reasoning based on their underlying terminating ordering. Constraint satisfaction techniques allow to delay the solving of constraint problems created by deduction steps.

The software developped in the project permit us to validate our ideas, to present our work to the scientific community, and to transfer our knowledge to application domains.

Activity reports: 2006 2005 2004 2003 2002 2001 2000 1999 1998 1997 1996 1995 1994