Automated reasoning (AR) is a field of computer science
concerned with turning computers into ever smarter thinking machines,
and injecting reasoning into computer applications.
AR is artificial intelligence (AI), symbolic computation (SC),
computational logic (CL), and it contributes to
the fundamental quest about what computing machines can do.
To date AR has developed primarily deductive methods that
build proofs (an argument by which something follows from something)
or models (e.g., a solution to a set of constraints, a counterexample),
and can be applied to settle conjectures about systems (e.g., programs, circuits,
data structures, communication protocols, mathematical structures).
Automated reasoners include theorem provers,
SAT-solvers (for SATisfiability in propositional logic),
SMT-solvers (Satisfiability Modulo Theories),
model checkers, and proof checkers, complemented with
libraries of theorems, and knowledge bases of computer-checked mathematics.
These tools can be integrated to form reasoning environments or
embedded as reasoning components inside other software systems.
My research includes theory, implementation, and application,
encompassing both synthetic
(e.g., design of reasoning procedures),
and analytic (e.g., analysis of their behavior) sides of computer science:
The documents distributed by this server have been provided by
the contributing authors as a means to ensure timely
dissemination of scholarly and technical work on a
noncommercial basis. Copyright and all rights therein are
maintained by the authors or by other copyright holders,
notwithstanding that they have offered their works here
electronically. It is understood that all persons copying this
information will adhere to the terms and constraints invoked by
each author's copyright. These works may not be reposted
without the explicit permission of the copyright holder.
(The copyright holder of papers published on journals is usually
the publisher of the journal. For conferences, the copyright holder is
usually the publisher of the proceedings, such as Springer, for Lecture
Notes in CS or AI, or ACM Press for ACM conferences.
The documents distributed by this server are the author's
personal copies of pre-prints of such papers. The final publication is available
from the copyright holder page (e.g., Springer) via the given DOI.)
Maria Paola Bonacina