Encoding and Solving a Problem
Food Chains
Food chains describe the feeding relationships between species in a biotic community.
They show the transfer of material and energy from one species to another within an
ecosystem.
If one species eats another, there is an food link from the eaten of
the food link to the eater of the foodlink.
Apex predators are those species that are not eaten by any species.
Primary producers (also known as autotrophs) are those species that do not eat any
species - they are capable of producing complex organic substances (essentially "food") from an
energy source and inorganic materials.
A sequence of food links from a species to a species to a species, etc, forms a food chain
that starts at the eaten of the first link and ends at the eaten of the last link.
A complete food chain starts at a primary producer and ends at an apex predator.
An apex predator is dependent on all the species in all the food chains that lead to the
apex.
The food chain environment can be modeled in typed first order logic, and various theorems can
then be proved.
Here the axioms of the system are given in English, interspersed with theorems that can be proved
from the preceding axioms.
- Axiom: The eater of a food link eats the eaten of the link.
- Axiom: The eaten and eater of a food link are not the same (no cannibalism).
- Axiom: Every species eats something or is eaten by something (or both).
- Axiom: Something is a primary producer iff it eats no other species.
- Theorem: If something is a primary producer then there is no food link such that the primary
producer is the eater of the food link.
- Theorem: Every primary producer is eaten by some other species.
- Theorem: If a species is not a primary producer then there is another species that it eats.
- Axiom: Something is an apex predator iff there is no species that eats it.
- Theorem: If something is an apex predator then there is no food link such that the apex
predator is the eaten of the food link.
- Theorem: Every apex predator eats some other species.
- Theorem: If a species is not a apex predator then there is another species that eats it.
- Axiom: For every food chain, the start of the chain is the eaten of some food link, and one
of the following holds:
(i) the eater of the food link is the end of the food chain,
xor (ii) there is a shorter food chain (shorter by one food link) from the eater of the food
link to the end of the whole food chain.
- Axiom: There is no food chain from a species back to itself (no death spirals).
- Axiom: A complete food chain starts at a primary producer, and ends at an apex predator.
- Axiom: Every species is in some complete food chain, i.e.,
(i) the species is the primary producer start of the complete food chain, or
(ii) the species is the apex predator at the end of the complete food chain, or
(iii) there is a non-complete food chain from the start of the complete food chain to the
species, and another non-complete food chain from the species to the end of the
complete food chain.
- Theorem: The start species of a complete food chain does not eat the end species.
- Theorem: If a species is neither a primary producer nor an apex predator, then there is a
food chain from a primary producer to that species, and another food chain from that species
to an apex predator.
- Axiom: Given two species, the first depends on the second iff there is a food chain
from the second to the first.
- Theorem: If a species is not an apex predator then there is an apex predator that depends
on the species.
- Theorem: An apex predator depends on all primary producers of all complete food chains that
end at the apex predator.
You must ...
- Formulate the types, axioms, and theorems in TPTP TFF syntax.
- Ensure that the axioms are consistent using an ATP system.
- Prove the theorems using an ATP system.
Submit one file containing all the axioms and conjectures, in the order they are listed above,
by 7th October.
Your submission will be graded according to the following:
- Types - 4%
- Axioms - 4%
- Consistent axioms 4% (only if seriously encoded)
- Conjectures 4%
- Provable conjectures 4% (only if seriously encoded and axioms are consistent)
It is worth 20% of the subject's assessment.
Please review the policies on assessment in the administration document.
Answers