Research
Automated reasoning (AR) is a field of computer science
concerned with enabling computers to reason, not necessarily like humans,
but rather in their own way, so that reasoning can be injected in 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.
AR methods build proofs (an argument by which something follows from something)
or models (a solution to a set of constraints or a counterexample),
and settle conjectures about systems (e.g., programs, circuits, data structures,
communication protocols, mathematical structures).
Automated reasoners include theorem provers, proof assistants, model builders,
validity checkers, SAT-solvers (for SATisfiability in propositional logic),
SMT-solvers (Satisfiability Modulo Theories), model checkers, and proof checkers,
complemented with libraries of theorems and proofs, and knowledge bases of computer-checked mathematics.
These tools may be integrated in reasoning environments or embedded in other software.
Selected topics in my work in automated reasoning include:
and my Research Summary
offers an overview with references to the publication list in the CV posted on my main web page.
COPYRIGHT NOTICE:
The documents distributed by this server are 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 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