On June 22, 2023 at 14:00 EEST, Marian Călborean (University of Bucharest) will give a talk in the Logic Seminar.
Title: Reasoning by brute force II. Implementing a natural deduction proof calculator for monadic predicate logic with minimal heuristics
Abstract:
One result of the ‘Logic and software’ elective course held at the Faculty of Philosophy, University of Bucharest was the interactive development of a natural deduction calculator that successfully proves exercises in classical textbooks. The calculator has versions in Python and PHP, both common programming languages, allowing the easy study and change of the software code corresponding to NK rules. It also uses brute force – running allowable rules until the conclusion is derived, then retracing the steps to display the shortest path to it; no backwards reasoning techniques were used. Since computational complexity required speed optimizations, a demonstration of their soundness and completeness is sketched.
The talk will take place physically at FMI (Academiei 14), Hall 214 “Google”.