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 posted on this page and its subpages are provided by the 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 other copyright
holders, notwithstanding that the authors have offered their works here. It is understood
that anyone downloading or copying in any way all or parts of these documents will adhere
to the terms and constraints invoked by each author's copyright. These documents may not
be reposted or distributed in any way without the explicit permission of authors and
copyright holders.
The copyright holder of a journal article is the author, if the article was published
open access, the journal's publisher (e.g., Springer, ACM) otherwise. The copyright
holder of a conference paper is the author, if the paper was published open access, the
proceedings' publisher (e.g., Springer for Lecture Notes in CS or AI, ACM for ACM
conferences) otherwise. The versions of journal articles and conferences papers posted
on this page and its subpages are the author's personal copies of post-peer-review
accepted pre-prints, but they are not the versions of record. The versions of record are
available via the given DOI.
Maria Paola Bonacina