Module for semi-automatic reasoning

0
ID: 
6.7
Workpackage: 
Case Study: Mathematics
Task leader: 
jordi.saludes
Assignees: 
jordi.saludes
Status: 
Planned

Automated reasoning is needed to assess the soundness of the model proposed by the student and to answer his/her questions. This requires adding small ontologies describing the word problem, including:

  • Data present in the problem statement;
  • Additional world knowledge to make reasoning possible.

Add State of the Art study here.

Set theory reasoning of the ducks and rabbits problem

Some time ago I managed to build a theory supporting the Farm problem in Isabelle/HOL (attached below)

I wasn't expecting such a toil but lack of detailed documentation and a wicked simplifier made my life miserable for a whole week.

Assumptions

It is based on 3 sets:

  • Being in the farm (farm)
  • Being a duck
  • Being a rabbit
  • and a function: is_leg_of : leg → animal.

    As axioms, we have:

Ground knowledge axioms

  • Rabbits have 4 legs.
  • Ducks have 2 legs.

Problem axioms

  • All animals in the farm are rabbits or ducks.
  • There are 100 animals in the farm.
  • There are 260 legs in the farm

Extra axioms

That is, facts that are implicitely known but you need to state for Isabelle with Main theory to work:

  • Rabbits and ducks are finite
  • Rabbits and ducks are disjoint

Variables and equations

Let R be the number of rabbits in the farm and D the number of ducks in the farm. With the preceding axioms, we were able to produce Isabelle-certified proofs that

R + D = 100

and

2*D + 4*R = 260

and then deduce that R=30 and D=70.

AttachmentSize
Farm.thy5.67 KB