search

Paradoxika / Skeptik

A library for Proof Theory (especially Proof Compression) in Scala.
33 stars 25 forks source link

Splitting Algorithm - Version 1.0 #115

Closed EzequielPostan closed 8 years ago

EzequielPostan commented 8 years ago

This is the first version of the First Order generalization of the Splitting algorithm. Improvements can be made, e.g. we can search for better conditions to examine which literals can be used for splitting.

The current version still fails in some cases, it tries to split the proof on literals that produces two proofs that can't be resolved after the splitting procedure. This happens in rare cases, but it must be corrected.

There are tests in the files FOSplit.scala and FOCottonSplit.scala that shows examples of the algorithm working properly.

ceilican commented 8 years ago

The current version still fails in some cases, it tries to split the proof on literals that produces two proofs that can't be resolved after the splitting procedure. This happens in rare cases, but it must be corrected.

In the meanwhile, please catch the exception and return the original proof, when the two proofs cannot be resolved.

ceilican commented 8 years ago

Thanks!

EzequielPostan commented 8 years ago

I caught the exception. I will upload this with the parsers pull request as this is a two lines correction.