Let PAC have one proof_attempt and remove goals When the ProofAttemptCofiguration only has one proof_attempt, there can only be a single goal. This can be retrieved through the proof_attempt.

Fix first_or_create! not knowing the display_name.

Move model filling methods into helper module.

Rename attribute hets_evaluator to importer.

Move concurrency handling to a separate class The new ConcurrentEvaluator is only used for Ontology parsing. It has all the functionality that the BaseEvaluator had before. The new BaseEvaluator, however, is the base class for the ProveEvaluator and does not contain any concurrency handling which renders the concurrency reladed methods in the ProveEvaluator needless.

Adjust collective proof attempt spec, fix evaluator.

Use predefined proof attempts in evaluation.

Use Prover model in ProofAttempt instead its name.

Use axioms for used_axioms.

Use Prover model in ProofAttempt instead its name.

Use axioms for used_axioms.

Rename variable hash to proof_info.

Use correct ID.

Rename proof attempt creating methods.

Add generated axioms model and create instances When proving, usually a logic translation is applied. Such a translation can introduce sentences as axioms that were not part of the original ontology/specification/theory. Those generated axioms need to be distinguished from the original sentences.

Add controller and view for proving.

Add used axioms to proof attempt.

Add ProveEvaluator to create ProofAttempts.