Larch is a prototype of an Intelligent Tutoring System that supports learning different proof methods (currently analytic tableaux for propositional logic and sequent calculi for intuitionistic logic).
Homepage It's a landing page for the project. Here you can learn more or head straight to the proof assistant (below).
Analytic Tableaux for Propositional Logic Step 1: Write down the formula.
Analytic Tableaux for Propositional Logic Step 2: Identify and select the main connective.
Larch has two target groups of users: Contributors (researchers) and Learners (students).
For Learners, Larch will be an intuitive web application for becoming proficient in the analytic tableaux method for propositional logic (and more proof methods in the future).
The main ideas behind the interface are: step-by-step assistance through the proof, effective hint system and engaging gamification features.
For Contributors, Larch is a highly customisable, modular and plugin-oriented engine coded entirely in Python. These features make it easier and quicker to implement new proof methods for different formal systems, and then move on from the command-line to the web interface.
<aside> 👀 Interact with the early prototype.
</aside>
<aside> 🧠 Visit the GitHub repo.
</aside>
Currently all technical documentation as well as friendly FAQs are only available in Polish on our internal website, but we will be translating them in the coming weeks.
Jakub Dakowski Founder & Chief
Łukasz Abramowicz Software Engineer
Barbara Adamska UX Specialist
Ola Draszewska Software Engineer
Dominika Juszczak Front-end Developer
Robert Szymański Research & Development
We are proudly supported by the Dean of the Faculty of Psychology and Cognitive Science at Adam Mickiewicz University in Poznań, Poland. Our main research advisor is dr Szymon Chlebowski from the Department of Logic and Cognitive Science.
<aside> 🌲 The truth is just a click away!
</aside>