Welcome, everybody.
Welcome, colleagues.
This is a joint talk with my two colleagues,
Saksham Attri from India and Aaron Windischbauer from Austria.
It's about GNU Aris.
It is a web application right now for students.
It used to be a native application written in C,
but now it's a C/C++ application for logic teaching
mostly at university level.
Thanks so much, Pilar, that you help us delivering this talk.
The logic education
software tool GNU Aris is quite well known
in the free software community,
has been developed since 2011 by a GNU activist, Ian Dunn.
It is no longer maintained by him, but the community,
started to work on the project and
now we have a new version and we have some new experiences
how it works in some school situations, some classroom situations.
This development was mostly based on the
Google Summer of Code 2023 project and the biggest
aim was to bring GNU Aris to the web application
and finally to try if the new features really applicable
in classroom situations for university students who attend a logic course.
You can ask the question: why another software tool?
There are a lot of software tools,
for example, the Coq system, Isabelle, Lean, and a lot
of others.
There are a lot of systems there to study mathematics or other
science research fields.
As I said, GNU Aris,
is not really new. Also,
we think that
the other big players
like Coq or
Lean or Isabelle, so they are
very good, very big, but maybe
too complex, too
big, too difficult for
prospective mathematics teachers.
So, at least
these young people who
want to teach mathematics for
the next generation, they are
usually not familiar with programming.
So, if they come
to learn
a system like Coq, it's really,
really exhausting.
It's really a big challenge
and that's why it
seems to be a good idea
to give them something
simpler.
The other idea, the
other concept is that
usually you don't have to give a whole
system for these... students,
prospective teachers.
Because
They usually need only a "taste" of the thing.
So they don't need the whole system.
They don't want to prove everything in mathematics.
They want to study just a small part of,
for example, number theory or a very small part of calculus.
It should be balanced between these two.
We need to have a quite good working, nicely working system.
On the other hand, it should be somewhat limited.
So the syntax should be very close to the everyday mathematics, to the school mathematics.
But of course, it's quite good if
there are still possibilities to reach a high level of mathematics in some sense.
Why GNU Aris? It's because it's open source.
It's complicated enough to tell some more complex stories
for our students.
But on the other hand,
not really ready for end users...
at least at that time we started this project we learned that it's
not easy to install it... among others...
so it has to be compiled and most students... most
mathematics teacher students... they don't have an idea on how to do it!
Of course it's possible to compile the software for many platforms:
for Windows, for Linux, for
Mac, and we did it but it's sometimes also difficult to do something in the classroom
even for university students because
the computer room is limited for a web browser, so
you don't... have any access to install new systems, new programs, so it's quite difficult...
so a web version... seems to be a good option.
Then the other thing is
that for
mathematics teachers: the native tongue. The mother tongue is of course preferred.
Then the import-export part of GNU Aris was also not really standard.
It's in XML format... we were thinking about that. And unfortunately the user can
experience some crashes in some situations. Well, in this slide you can
see how the old version looked like.
It's a modern system in some sense, so it has
a so-called GTK interface.
Well, you can see: on the top there is a menu.
Then statements that are commented with arbitrary
long texts.
Then you can tell if this line is a... is a premise or
maybe a conclusion of the older... premises and
while "dm" is the De Morgan rule
so any
line here is kind of application of the De Morgan rule
Yes, so back to Google Summer of Code.
We are very grateful to Google that they supported this project.
Mostly the work was done by Saksham in India.
It was three months of very active work with some support by two more students
Andreas Ebetshuber and Alexander Thaller and I was
responsible for mentoring the whole project. We had a work plan.
It's necessary when you start some of Google Code project.
It consisted of five
big steps to create a so-called Qt interface. The Qt
system
allows programming in a framework, C++ framework.
And because of that, it was possible to compile the whole system
into HTML and WebAssembly, which means much more flexibility.
Then the interface had to be polished a bit.
We published a new version, and then we started to get user feedback
and to fix issues.
Maybe you want to know what is this big A here.
This is the logo of GNU Aris, and it was designed by Ian Dunn,
original developer of the program.
So he is Saksham.
He is a young student in India, and he worked hard on the implementation.
He takes the lead now and gives some details on the implementation.
I will now explain the architectural.
design for the Qt application.
Here, we have tried to emulate the famous model-view-controller framework.
So, the user's interaction is limited to the view, which, in this case, is provided
by the QML UI.
If the user request exceeds capabilities built into the UI, then the request is forwarded
to a C++ controller layer, along with the relevant proof data.
This middle layer now processes the data into
appropriate C data types, and forwards it
to the C logic engine.
We are reusing the old logic engine
by decoupling the GTK UI with program logic.
Thus, the generated results are communicated back to the controller,
which then updates the view
so that the results are displayed to the user.
While the new interface is a bit different from the GTK interface, it was quite important
to create a new kind of user interface that is transparent in the sense of working in
a native environment, so natively in Windows, on Mac, on Linux, but also to be able to
translate it into the web.
So what you can see here, this is the native version of the new Qt version,
again with the same premises and the same conclusions.
Conclusion is the notion here in GNU Aris.
And the menu system is a bit different, so here you can open the menu,
and also there is a virtual keyboard to
enter logical operations and some other symbols,
finally this button here is responsible for checking if you
typed the input correctly or not... so if it is not correct then you will get a red
color here... the other interface... the web interface is
quite similar... of course there are some very
minor differences. This example here is a bit different and you can see that there is
an option to write the mathematical symbols... somewhat differently
okay so let's start this
program... if you... start GNU Aris... well yeah maybe it's...
it's not bad to start it again
so in
in background the WebAssembly code is compiled and here this is one
input line... well I add a statement A and I add a new premise:
statement B and then I add the conclusion:
it's A and B. A and B is a conclusion.
Now if I try to check if it is okay, then we get an error message...
that... well, there is a default rule set and a default rule and
here we didn't really use the
inference... the inference group and modus ponens but we used something different...
here we used the
conjunction and now if you click on it, it is still an error because we need to give the references
to the premises.
So what is the first premise... first
reference: this one and this one, so the cursor needs to be here and we need to click on the
reference so now we can see that this conjunction is related to one and two... or is this based on
these two premises and if we click on evaluate and we get this answer. Well, if we remove something,
you can try it again... you can see that those lines that are syntactically correct,
they are still green. Only those lines that have some problems in the background: they are red.
Back to the presentation. We managed to hold a series of lectures on logic. My former student
and my colleague now,
Aaron, was one of these 30 students between October 2023 and January 2024.
So he also tried the program, he gave feedback, and some examples were done by him.
Well, this logic course discussed two main topics, propositional logic and first-order logic.
Of course, 15 weeks are not too much for such big topics.
With GNU Aris... GNU Aris was not the only software system we used...
to visualize, to explain some concepts of logic, we used other systems,
for example, GeoGebra Discovery, or a SAT solver, MiniSAT.
Mathematica, Wolfram Alpha for propositional logic too.
Here we would like to illustrate GNU Aris with two examples.
One example is from a quite well-known book, from Raymond Smullyan,
the famous logician, The Lady or the Tiger.
And the second example is a well- known basic concept from category theory.
So let's have a look.
The first example is shown in German, because this is how it is authentic. :-)
It's about a king who gives a puzzle for the prisoners.
So maybe you want to see this question in English.
The basic idea will be explained in the next slide.
So the king...
tries to find good puzzles
for the prisoners.
Well, let me read this.
Yesterday was a fiasco, said the king to his minister.
The three prisoners solved their puzzles.
Well, we have five trials coming up today, and I think I'll make them a little tougher.
"Excellent idea", said the minister.
Well, in each of the trials of this day, the king explained that in the left-hand room
(room 1), if a lady is in it, then the sign on the door is true.
But if a tiger is in it, the sign is false.
In the right-hand room (room 2), the situation is the opposite.
A lady in the room means the sign on the door is false, and the tiger in the room means
the sign is true.
Again, it is possible that both rooms contain ladies or both rooms contain tigers, or that
one room contains a lady and the other a tiger.
This is the English explanation, the English story of the puzzle.
So the puzzle is exactly the fifth trial.
Same rules apply, and here are the signs. At least one room contains a lady,
room one, and room two, the other room contains a lady. So this is the fifth puzzle. Here
you can see the Hungarian version of this book, a very famous, very well-known book.
And here Aaron shows the German translation, also quite popular.
Now Aaron will tell you
some words how he solved this problem when he was a member of this course.
As already stated, this is my solution to Smullyan's fifth trial in the web version of GNU Aris.
I started with premises which represent the rules of the trial,
where L and T followed by a number
to indicate that there is a lady or a tiger in that specific room.
S1 and S2 refer to the signs of
each room. Then I initiated a sub- proof with the assumption of a lady being in room 2.
With the rules of the trial, I deduced that the assumption leads to a negation of sign 1,
which means there is no lady in any of the rooms.
This leads to a contradiction with the assumption that there
is a lady in room 2.
This figure shows how I used that contradiction, which indicates that a tiger
must be in room 2. With that information,
I deduced that the sign of room 2 is true,
and therefore a lady has to be in room 1.
I finished the proof by showing that a lady in
room 1 does not lead to a contradiction.
A lady in room 1 means that the statement of sign
one of at least one room
containing a lady is true
which does not contradict that
a lady is in room one. The final
line is the solution of the puzzle.
The prisoner should pick room one
since that room contains a lady.
The second
example about
a so-called binary operation
is denoted
by O. It has
two parameters
and we assume that this operation
is commutative.
Because it
is assumed for each a
and for each b. And we
assume that there is
a so-called
right
identity element
which means that for each a
this binary operation
delivers a.
So this is a kind
of neutral thing or
as other formulated
it's a right
identity. Then by
using some rule
we can learn that for each a is "a operation e_" equals a so this
is because the second statement this is a so- called existential instantiation
in GNU Aris. Then you can use the commutative property
and so on... so for each step there was a rule in GNU Aris.
Finally you can learn that there is an "f", element of the main set that
this identity also holds.
So a right identity
element is also a left
identity element.
And vice versa, it's not
shown here.
What kind of feedback we get
from the other students,
from the other 29...?
And also Aaron
was giving some
feedback. Well, the
error messages are not very
easy to understand
for simple
users. It's for programmers
more or less and not for
simple users
like prospective mathematics teachers.
Then it
should be not bad if
some more feedback would
be given for the user if there is
an error. Some
devices are not really supported if
they have a small display.
This is not very good
at the moment yet.
Changing the language
to a different one
than English... still
on the wishlist.
Copying, pasting, highlighting inputs, or to change the input type, of a statement...
is a technical question, but it should be nice to work.
And also the exclusive disjunction and the contrapositive,
they were missing for many proofs, and therefore our proofs were quite long.
And some ideas could be implemented for the next year,
so maybe we can have some more reports then.
And that's all. Thank you so much for being here,
and we want to share some references that could be interesting if you want to learn more on this.
Well, we will hopefully continue this project...
in the next months, and we would like to do some more...
if possible. Thank you so
much. We wish you a great
conference evening
and see you soon
hopefully in person.