The area of this project is automated reasoning, or how to make computers reason, not necessarily
like humans, but rather in their own way.
Within automated reasoning, automated deduction focuses on methods based on logic, because
logic provides us with a language for the machine to reason with. Problems are typically represented
as validity queries (e.g., does a conjecture follow from a set of assumptions?) or satisfiability queries
(e.g., does a set of constraints admit solution?), where conjecture, assumptions, constraints are
logical formulae, expressing properties of an object of study (e.g., a system, a program, a data type,
a circuit, a protocol, a mathematical structure). Answer to a validity query is either a proof or a
counter-example. Answer to a satisfiability query is either a solution or a proof that none exists.
This is a project on semantic guidance in automated deduction. Most past and ongoing work in
deduction adopted primarily syntactic approaches. This project is concerned with a different style of
reasoning, that we call Semantically-Guided Goal-Sensitive reasoning, or SGGS for short.
The distinguishing features of SGGS are (a) a very expressive logic, namely first-order logic; (b)
semantic guidance by an initial interpretation, that gives the machine a notion of what is true and
what is a false in one state of the world; (c) goal sensitivity, or sensitivity to the conjecture to be
proved; (d) dynamic construction and update of a model of the set of clauses for which a proof is
sought; and (d) proof confluence, which means that the machine does not need to undo already
committed steps to return to previous states in the search for a proof.
This project has the following objectives: (I) Design of the algorithms and data structures required by
SGGS reasoning; (II) Implementation of the first SGGS theorem prover; (III) Experiments with the
SGGS prover.