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. One species eats another if and only if 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 auxotrophs) 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. 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 modelled axioms in typed first order logic, and the following theorems can then be proved. Note that some of the theorems need less axiomatic background, so you should work incrementally adding axioms until another conjecture(s) can be added and proved. As ATP systems correctly process only one conjecture at a time, you will have to comment out the conjectures other than the one to be proved.

If something is a primary producer then there is no food link such that the primary producer is the eater of the food link.
Every primary producer is eaten by some other species.
If a species is not a primary producer then there is another species that it eats.
If a species is an apex predator then there is no food link such that the apex predator is the eaten of the food link.
Every apex predator eats some other species.
If a species is not an apex predator then there is another species that eats it.
The start species of a complete food chain does not eat the end species.
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.
If a species is not an apex predator then there is an apex predator that depends on the species.
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 conjectures in TPTP TFF syntax.
Ensure that the axioms are consistent using an ATP system.
Prove each theorem from preceding axioms using an ATP system.

You can get a jump start by asking your favourite AI assistant to do it. I tried that, but the encoding is sloppy. You'll need to improve it by hand.

Your submission will be graded according to the following:

Formatting and comments - 2%
Types, nicely organized before the axioms - 2%
Consistent axioms, in a sensible order - 2%
Conjectures, inserted between the axioms as early as possible 2%
Provable conjectures 2% (only if seriously encoded and axioms are consistent)
Demonstration of understanding to Geoff or Lucas or Laura - -10% to 0%

This part is worth 10%.

A Freshwater Pond

In a freshwater pond there are the following complete food chains:

Algae → Zooplankton → Fish → Heron
Algae → Zooplankton → Frog → Heron
Algae → Insect → Frog → Heron
Duckweed → Snail → Frog → Heron
Pondweed → Insect → Fish → Heron
Pondweed → Snail → Fish → Heron

The foodchains capture all the species that exist (you'll need to encode that), and all those species are different (you'll need to encode that). Add axioms to record which species eat which species, assuming that the food chains capture everything that each species eats. Add an axiom(s) that defines "trophic level": primary producers are at level 0, species that eat primary producers are at level 1, etc.; a species can have multiple trophic levels. Some Food Chain axioms are probably necessary too, so keep adding to the same file - just comment out the Food Chain conjectures while working on this part.

Encode the following conjectures, and use ATP to decide which of these are theorems. For those that you decide are theorems, add a comment %----Proved on the line immediately before the conjecture. For those that you decide are not theorems, add %---- commentary on lines immediately before the conjecture explaining how you came to that conclusion.

Algae is a primary producer.
Heron is not an apex predator.
A fish is neither a primary producer nor an apex predator.
Frogs and fish eat all the same species.
There are two complete food chains that end at heron, but start at different species.
Snails depend on herons.
Fish have a trophic level that is greater than a trophic level of a snail. (Challenge: Prove it for all trophic levels of fish and snails.)
There is a species with a trophic level greater than at least one of the trophic levels of a heron.

Your submission will be graded according to the following:

Formatting and comments - 2%
Species' types and axioms - 2%
Trophic level types and axioms - 2%
Conjectures (after all the axioms) - 2%
Provable conjectures - 2% (only if seriously encoded and axioms are consistent)
Demonstration of understanding to Geoff or Lucas or Laura - -10% to 0%

The part is worth 10%.

Submission

You must submit one .p file in TUWEL. The file must contain, in this order:

A comment line %----Food Chains
The type annotated formulae for the Food Chains part.
The interleaved axiom and conjecture annotated formulae for the Food Chains part.
A comment line %----Freshwater Pond
The type annotated formulae for the Freshwater Pond part.
The axiom annotated formulae for the Freshwater Pond part.
The conjecture annotated formulae for the Freshwater Pond part.