Research | Laboratory for Automated Reasoning

Activities

The activities carried out in the laboratory concern the study, analysis and use of software for automatic reasoning. The main software used in the laboratory are theorem provers such as Vampire, SMT solvers such as Z3 and computational algebra software such as Prover9 and Mace4. More specifically, the aforementioned software is combined with theoretical results concerning multi-valued logics to build tools for vague reasoning or reasoning in the presence of uncertainty.

The Laboratory is equipped with four workstations and 3 Apple desktop computers that can be used for writing software, for drafting the thesis and for bibliographic activities. A whiteboard and audio recording system is also available.

Students and Traineeships

The Automatic Reasoning Laboratory is accessible to students for the following purposes:

• carrying out internships and internships for Mathematics and Computer Science students of the University of Salerno and for students of the Erasmus + program;
• writing master's thesis in Mathematics and Computer Science;
• carrying out research activities for PhD students in Mathematics.