Interactive mode to explore logics

[rzach]

Since MUltlog offers a convenient way of converting different specifications of finite-valued logics to an internal representation that can then be manipulated by Prolog, it would be nice to have a way to run MUltlog interactively to do things like:

• [x] Load an .lgc file into the database using an identifier (so that different logics can be loaded simultaneously).
• [ ] Export a logic to an .lgc file.
• [x] Pretty-print truth tables of a logic.
• [ ] Interactively change a logic, e.g.:
  • [ ] Replace a value in a mapping.
  • [ ] Replace or add mappings using the lgc format.
  • [ ] Copy operators/mappings from one logic to another.
  • [ ] Define an operator using a formula.
• [x] Compute the value of a formula in a logic, or find values that result in a given formula.
• [x] Determine if a formula is a (non)tautology, if an entailment holds.
• [x] Determine if two formulas are equivalent (within or between logics).
• [x] Find tautologies of a logic.
• [x] Find formula equivalent to a given one.
• [ ] Compute new logics from old ones, e.g.:
  • [x] direct product of two logics.
  • [x] factor logic by a strong congruence relation.
• [x] Find a (smaller) homomorphic image of a logic.
• [ ] Interactively compute CNFs and rules.
• [x] Test if two logics are isomorphic.

[rzach]

Started on this -- it's in ml/ml_interactive.pl

loadLogic('goedel.lgc', gl) loads & checks an LGC file and makes it available using gl.

Then you can do things like :- isTaut(gl, imp(X,X)). to check if X -> X is a tautology.

It would be better/standard practice to have the gl as the last argument, right?

Formulas are terms possibly with variables, so that you can use Prolog to search for truth values etc.

I tried but failed to make a generator for formulas of a given logic. isFormula(gl,X) will just list all the formulas you can form from neg, true, and false, and never list the ones involving and, or, imp, etc. I mucked around with different ways of forcing breadth-first search, by working with polish notation as a list, but didn't get far.

Why? I wanted to be able to have a way of saying findTaut(X) and then have Prolog find all the tautologies. isTaut(X) doesn't work for this because it forces all variables to be truth values. What's the best way of doing that?

[rzach]

BTW to activate interactive mode just say multlog.