v0.9.0

What's Changed

• Newly added support for saving and loading Lohika scripts to and from files.

Full Changelog: v0.8.0...v0.9.0

v0.8.0

What's Changed

• Comments by @melvic-ybanez in #46
• Fix for the issue of the leading whitespaces in derived entailments

Full Changelog: v0.7.0...v0.8.0

v0.7.0

This release added support for function definitions:

Full Changelog: v0.6.0...v0.7.0

v0.6.0

Updates

This release added support for predicate definitions and recursive unfolding.

For instance, consider this derived entailment:

P(a, b) := Q(b, a);
R(x) := S(x) & A:xS(x) & P(x, x);
A:x, y[P(x, y)], R(y) |= Q(b, c)

It is expected to unfold to the following:

A:x, yQ(y, x), S(y) & A:xS(x) & Q(y, y) |= Q(b, c)

Full Changelog: v0.5.1...v0.6.0

v0.5.1

This is a quick fix for the issue on name generation when the given base name ends with z.

Additional Contexts

When Lohika performs a standardization, it generates a new set of unique names, each based on a particular string called a base name, that will be used to remove potential name clashes.

During name generation, Lohika will take the last character of the base name.
If it is a letter, Lohika will change it into the next letter of the alphabet. If the resulting new name already exists, Lohika will try the next letter and repeat the process until it reaches z, in which case Lohika will move back to a (it doesn't always start with a, after all) and repeat the process. The second time it reaches z, Lohika will try appending numbers.
If, on the other hand, the last character is a number in the first place, Lohika will just increment that.

This fix is needed because the implementation made an off-by-one error resulting to characters outside of the english alphabet.

Full Changelog: v0.5.0...v0.5.1

v0.5.0

What's Changed

• Propositional Variable Definitions by @melvic-ybanez in #39

Full Changelog: v0.4.0...v0.5.0

v0.4.0

Main Changes

• A simple query editor has been added (see image below).
• Changes in logical operator symbols:
  • Implication changed from => to ->
  • Biconditional changed from <=> to <->

New UI with the Editor:

Full Changelog: v0.3.0...v0.4.0

v0.3.0

This release removes the need for Skolem suffixes and replaces them with entailment-wide standardization and skolemization. #31 explains it in details, including how it solves the issue on name clashes with generated Skolem functions.

Full Changelog: v0.2.1...v0.3.0

v0.2.1

Updates

This release contains an important hotfix for the issue of the uniqueness of Skolem function names across formulas.

For instance, in the previous release, the following would hold:

A:xE:yP(x, y), A:xE:y!P(x, y) |= Q(a)

It shouldn't have. The ys in the premises are not guaranteed to have the same values. The problem here was that, during Skolemization, the two variables were replaced with the same function name. While function (and constant) names are unique within a formula (due to standardization and alpha-conversions), they weren't guaranteed to be unique across multiple formulas in the entailment. Lohika therefore decided that the premises in the example above could be unified and were complementary, leading to a contradiction.

To resolve this, I added what I called a skolem suffix, an integer identifying the formula based on its position in the entailment. It's just a generalization of the const suffix I used for the Skolem constants to resolve the same issue of uniqueness for constants.

The Skolem suffixes are rendered as subscripts, as shown here:

Now, the two premises could no longer be unified, and the entailment failed to hold, as desired.

Full Changelog: v0.2.0...v0.2.1

Edit: This fix is only partial, as the user can still name their constants, functions, and existential variables with skolem suffixes, thereby still causing potential name clashes. A more permanent solution is discussed in this issue.

v0.2.0

Main Updates

1. Support for first-order logic. Statements involving universal and existential quantifiers, predicates, functions and constants, are now valid logical queries.
2. Faster resolution and shorter proofs. In the previous release, Lohika will sometimes fail to see that a contradiction, if any, already exists, and might continue to derive new clauses, until those contradictions are eventually found. This made some proofs longer than they needed to be. In this release, Lohika will pick up contradictions as soon as they are introduced.
3. Bug fixes.

Full Changelog: v0.1.2...v0.2.0