Equality Logic is EMBEDDED in Multiple Form Logic

The engineering symbol for the NAND connective (the 'stroke') can be used to build any propositional formula. The notion that truth (1) and falsity (0) can be defined in terms of this connective is shown in the sequence of NANDs on the left, and the derivations of the four evaluations of a NAND b are shown along the bottom. The more common method is to use the definition of the NAND from the truth table.Image via Wikipedia

Sometimes I struggle to understand certain types of Computer Science papers, that look as though a PhD in Pure Maths is a minimum prerequisite, to understand them. Sometimes, though, elegant possibilities for simplifications seem to exist, of which the authors are (probably) unaware; important simplifications based on deeper levels of knowledge; also… simpler than conventional Logic.

E.g. In their paper «Transforming equality logic to propositional logic» (PDF-file; click to download) the authors (Hans Zantema and Jan Friso Groote) «investigate and compare various ways of transforming equality formulas to propositional formulas, in order to be able to solve satisfiability in equality logic by means of satisfiability in propositional logic«.

Well, I am currently working on this paper, trying to improve the algorithms (for equality logic) through a different paradigm, Multiple Form Logic.

  • In Multiple Form Logic, equality is the absolute negation of (any form of) distinction.

The fundamental concept here is -of course- «distinction«. The three axioms of Multiple Form Logic ensure that (from a Boolean perspective) all the nice and useful properties of Propositional Logic are (again) valid, but they are available at a reduced price or lower complexity, in terms of human (as well as mechanical) theorem-proving costs.

Now, the distinction between two (distinctions) X, Y can be depicted as:

difference_x_y2.jpg

Equality definitions (such as those used by the previous paper) are superfluous: They are already EMBEDDED inside Multiple Form Logic! I.e. you don’t need to «define» any «equality substitution», in M.F.Logic, because it already exists (built-in) inside a much simpler and a much more fundamental system, and (by Occam’s razor) it can and it should replace Propositional Logic!

So, to define «equality»,as «the absolute negation of (any) distinction», we may first ask: – What is the «absolute» negation of something?

  • It is the distinction between it (the thing itself) and every (other) thing…
  • where a symbol for «every (other) thing» (in the universe) is The Boolean value «1»…
  • which also corresponds to. the Absolute Oneness of Everything; i.e. …
  • where everything else is already included (inside it, inside this «1»).

So, «equality between X and Y» in Multiple Form Logic can be depicted as:

equality1a.jpg

In page 3 of their paper, Hans Zantema and Jan Friso Groote express some Basic Boolean definitions and properties, which are right from the start (as usual)… a litle superfluous:

2 Basic definitions and properties
Let A be a finite set of variable symbols. We define an equality formula by the syntax

V ::= x | y | z | · · ·
where A = {x, y, z, . . .}

E ::= V = V | true | false | ¬E | (E _ E) | (E ^ E) | (E ! E) | (E $ E)

Hence an equality formula consists of equations «x = y» for x, y in A and usual
boolean connectives…

Well, there are (not-so-obvious) advantages, by not beginning this way, but (e.g.) definining equality, X = Y, to signify «absolute negation of (any) distinction between X and Y»….

  • The advantages of such an approach include «beneficial side-effects».
  • E.g. that… Prolog-like variable – unifications become possible…
  • …through methods that seem deceptively «too simple» or «too Boolean».

These «positive side-effects» have already been discussed in chapters 17 and 18 (of the M.F.Logic site):

Hans Zantema and Jan Friso Groote said, in their abstract:

In this paper, the authors first define an «equality substitution«, which they then compare to certain methods of «bit-vector encoding« (while proving the soundness and consistency of their approach) and finally (in the last section of the paper) they «report some experiments showing that equality substitution outperforms the bit vector encoding for a class of formulas similar to the pigeon hole formulas».

Well, in another article of this blog

  • I will attempt to offer an alternative methodology for Equation Logic, comparable to the one above but (hopefully)… a lot more more efficient.
Related articles

.

7 comments

  1. Πολύ καλό άρθρο. Βλέπω ασχολείστε με λογικό προγραμματισμό, έτσι εξηγείται η εξαιρετικά ψαγμένη απάντηση, για την λογική, στην καλύβα. Αν γράφεται συχνά για λογικό προγραμματισμό θα είμαι συχνός επισκέπτης.

    Κάτι που θα ήθελα να συμπληρώσω, είστε ο πρώτος έλληνας προγραμματιστής που βρίσκω, ο οποίος στο ιστολόγιό του ασχολείται και με άλλα θέματα, εκτός προγραμματισμού.

  2. Αγαπητέ emporas,
    Ευχαριστώ για την (απροσδόκητα) θετική γνώμη. Συνήθως τέτοια θέματα μερικοί τα “παίρνουν στο ψιλό”, ενώ άλλοι νομίζουν ότι… πάω να μπερδέψω τον αναγνώστη με τεχνικά θέματα που δεν είναι εύκολα προσιτά (αν δεν είναι περίπου συνάδελφος).
    Πάντως, ναι, θέλω να γράψω συχνότερα για λογικό προγραμματισμό, και φυσικά για τη Λογική την ίδια. Ασχολούμαι πολλά χρόνια με μια ιδιότυπη θεωρία, όπως θα είδατε, η οποία (εκτός των τεχνικών πλεονεκτημάτων της) προσφέρει και… μεταφυσική ή φιλοσοφική απόλαυση. Πραγματικά δεν είναι λίγο, αν καταφέρουμε να ενοποιήσουμε τη Λογική με το χώρο της Φαντασίας και του Εσωτερικού Κόσμου. Πολλοί άνθρωποι στον κόσμο εδώ και πολλά χρόνια δουλεύουν σε αυτή την κατεύθυνση. Π.χ. ο Ben Goertzel κατάφερε να εξάγει περίπου τη μισή… κβαντομηχανική σαν λογική συνέπεια των ιδιοτήτων μιας δικής του (παρεμφερούς) Λογικής Άλγεβρας (”Ons Algebra”) που επεκτείνει την αρχική δουλειά του George Spencer Brown. Θα βρείτε πολλά υλικά για αυτό το θέμα στα site που αναφέρω.
    Τα τελευταία χρόνια υπάρχει διεθνής οργασμός έρευνας γύρω από τις βάσεις της λογικής, ιδίως όσον αφορά το “Satisfiability” της απλής (φαινομενικά αστείας) άλγεβρας Boole. Αν και το πρόβλημα είναι “NP-complete”, δηλαδή πολύ δύσκολο, ευριστικές λύσεις έχουν βρεθεί που το λύνουν σχετικά γρήγορα, για πολύ μεγάλο αριθμό μεταβλητών. Και το δικό μου ενδιαφέρον για το πρόβλημα “SAT” έχει ανανεωθεί μετά από όλα αυτά, γιατί έχω ενδείξεις (όχι αποδείξεις ακόμη) ότι η χρήση του τελεστή XOR και άλλα χαρακτηριστικά της λογικής δομής που ερευνώ, θα προσφέρουν νέες σημαντικές επιταχύνσεις και την επίλυση του προβλήματος “SAT” (στο οποίο μπορούν πια να μεταφραστούν ΟΛΑ τα άλλα παρόμοιας δυσκολίας προβλήματα -τα “NP-complete”). Δεν είμαι βέβαια σίγουρος αν αποδείξουμε έτσι και το μαγικό “άγιο δισκοπότηρο” της Λογικής, την ισότητα “P=NP”, που παραμένει αναπόδεικτη, αλλά πάντως… κάθε βελτιστοποίηση είναι οπωσδήποτε καλοδεχούμενη παντού.
    Ο λόγος που μιλάω για άλλα θέματα εκτός προγραμματισμού, σε αυτό το ιστολόγιο είναι βεβαίως ότι ο στόχος μου είναι φιλοσοφικός, κυρίως. Είναι πλέον δεδομένο (αποδεδειγμένο) ότι ΟΛΟΣ ο προτασιακός λογισμός μηδενικού βαθμού προκύπτει σαν συνέπεια τριών μόνο προτάσεων, εκ των οποίων μόνο η τρίτη είναι αξίωμα και οι άλλες δύο πηγάζουν από “κατασκευές της εμπειρίας”. Το τρίτο αξίωμα είναι συναρπαστικό γιατί δείχνει το ρόλο της φαντασίας και του εσωτερικού μας κόσμου μέσα στη λογική, σαν διαδικασία “αντιστρέψιμης εσωτερίκευσης”. Το πρώτο αξίωμα είναι μία “φαντασίωση απολυτότητας” που προκύπτει 100% κατασκευαστικά (Εν το παν, επομένως η ένωσή του με οποιοδήποτε πράγμα ισούται με τον εαυτό του). Το δεύτερο αξίωμα μπορεί να συγκριθεί με την εμπειρία ενός παλτού που το φοράμε αφού “κάνουμε το μέσα έξω” δύο φορές, οπότε… ξαναγυρίζει στην αρχική του θέση. Με βάση μόνο αυτά τα αξιώματα και ΤΙΠΟΤΕ άλλο, προκύπτουν ΟΛΟΙ οι “κλασσικοί” νόμοι όπως π.χ. η μεταβατικότητα της συνεπαγωγής (ότι αν Α συνεπάγεται Β, και Β συνεπάγεται Γ, τότε Α συνεπάγεται Γ). Το αποτέλεσμα είναι συναρπαστικό και επαναστατικό. Η λογική δεν περιγράφει πιά ούτε “αυτονόητα” φαινόμενα του υλικού κόσμου, ούτε… απόκοσμα και αποκομμένα από την Εμπειρία αξιώματα, αλλά περιγράφει τη διαδικασία της νόησης και της φαντασίας καθώς αυτή αντιλαμβάνεται τον εξωτερικό κόσμο, μάλλον αυθαίρετα, αφού “τα όρια μπορούμε αρχικά να τα χαράξουμε ΟΠΟΥΔΗΠΟΤΕ επιθυμούμε”. Ετσι εξηγείται ακόμη και η… τηλεκίνηση, ή η τηλεπάθεια, σαν φαινόμενα που προκαλούνται από ανθρώπους που χαράσσουν με ιδιόρρυθμο τρόπο τα δικά τους “όρια του εγώ” μέσα στον κόσμο.
    Η παλινόρθωση της φαντασίας και του εσωτερικού κόσμου και η αποκατάστασή τους μέσα στην επιστημονική μας σκέψη, ασφαλώς θα κάνει… τους σουρεαλιστές να χαρούν πολύ! Αλλά… αυτό το κάνουμε πλέον χωρίς κανένα απολύτως δόγμα, αφού όλα τα δόγματα είναι στην πραγματικότητα… Λογικό Λογισμικό!
    Περισσότερα… στα επόμενα “επεισόδια”!

  3. Αυτά τα θέματα ακόμα και να είναι συνάδελφος(προγραμματιστής μάλλον θα εννοείτε) δεν είναι απαραίτητα κατανοητά αν δεν έχει ασχοληθεί συγκεκριμμένα με λογικό προγραμματισμό, και γενικά με την μελέτη της θεωρίας της λογικής. Προσωπικά απο όλους τους προγραμματιστές που έχω γνωρίσει, δεν ξέρω κανένα να ασχολείται με τέτοια θέματα, καθώς είναι περισσότερο επιστημονικού ενδιαφέροντος και λιγότερο πρακτικού.

    Αυτές τις φιλοσοφικές προεκτάσεις της λογικής δεν τις ήξερα και είμαι ιδιαίτερα περίεργος να τις μάθω. Απο την κλασσική περιήγηση που κάνει κάποιος όταν μπει σε ένα ενδιαφέρον ιστολόγιο, είδα πως ασχολείστε και με την Prolog, η οποία είναι φανταστική γλώσσα, και όπως επισημαίνετε θα έρθει στο προσκήνιο τα επόμενα χρόνια.

    Στο προηγούμενο σχόλιο είπα, πως ενθουσιάστικα που βρήκα ένα προγραμματιστή που ασχολείται με φιλοσοφία, γιατί γενικά τα geeks, αν και μέσα στην τεχνολογία, διακατέχονται απο μονομερείς και κολλημένες απόψεις. Η επιστήμη των υπολογιστών έχει πραγματικά ανάγκη την προσέγγιση με ανοιχτούς τους ορίζοντες, το οποίο προϋποθέτει όμως μια πολύπλευρη μόρφωση. Είμαι πολύ περίεργος να διαπιστώσω και εγώ αυτήν την μεταφυσική απόλαυση.

    Αν και τα τελευταία χρόνια ασχολούμαι, όπως όλοι, και εγώ με τις γλώσσες της «μόδας» θέλω οπωσδήποτε να ξαναασχοληθώ με Prolog, Lisp, γενικά όλη αυτή την θεωρία. Αν όμως αυτός ο τομέας δεν είναι η δουλειά σου και έχεις ένα σωρό άλλα πράγματα να κάνεις(κατασκευή σελιδών, προσωπική ζωή, blogging, φιλοσοφία, κλπ) είναι πάρα πολύ δύσκολο να παρακολουθήσεις τις εξελίξεις και σε αυτόν τον τομέα, γιατί είναι πραγματικά άπειρος, σειρές δεκαετιών απο έρευνα. Χαίρομαι πολύ λοιπόν που σας βρήκα, να ενημερώνομαι απο πρώτο χέρι για την αιχμή της τεχνολογίας, και τις εξελίξεις απο ένα υπεύθυνο και μορφωμένο άτομο, πάνω σε αυτό το εξαιρετικά ενδιαφέρον αντικείμενο.

    Θα ξαναρίξω μια ματιά στα θεωρητικά κομμάτια και στην Prolog, για να μπορώ να σας παρακολουθώ. Της δουλειάς είμαι και εγώ, δεν χρειάζεται να μου εξηγείτε τι είναι NP πληρότητα τα καταλαβαίνω.

    Aνυπομονώ για τα επόμενα επεισόδια.

  4. Αγαπητέ emporas,
    Αποτελεί… ευτύχημα (ίσως) το ότι αυτές τις μέρες έχω πολύ ελεύθερο χρόνο να… μπλογκάρω ακάθεκτος, αν και έχω αναλάβει μία δουλειά στο σπίτι, να γράψω ένα scheduling optimising software (σε SWI-Prolog) για ένα φίλο, που έχει την Εταιρεία “PSP Ltd”, τον Λάμπρο Χρονόπουλο.
    Ιδιαίτερα ευγνώμων πρέπει να είμαι και στον νέο φίλο (μέσω διαδικτύου) Ralf Barkow, για το χθεσινό του άρθρο. Σε αυτόν απευθύνω το εξής σχόλιο:
    I am very grateful for Ralf’s recent blog-article presentation of my Theorem Proving Software (of 2003) that proves (and automatically annotates with proof-step explanations) Logic Expressions in Multiple Form Logic: The article is here. (click to see it).
    Πρέπει να κάνω… ασκήσεις διαλογισμού στη Σεμνότητα, γιατί αν καβαλήσω κάνα καλάμι, ούτε το… καλύτερο Prolog Back-tracking, δεν με σώζει. (I said, Ralf, that if I allow myself to become arrogant, at this stage, not even the best Prolog back-tracking mechanism will help me… recover from it; So I am grateful as well as -hopefully- modest! -hehe).
    Τα λέμε σύντομα και ΠΙΟ εκτενώς, αφού είστε ήδη κατηρτισμένος σε θέματα όπως το NP-completeness…
    Με εκτίμηση
    Γιώργος

Σχολιάστε

Εισάγετε τα παρακάτω στοιχεία ή επιλέξτε ένα εικονίδιο για να συνδεθείτε:

Λογότυπο WordPress.com

Σχολιάζετε χρησιμοποιώντας τον λογαριασμό WordPress.com. Αποσύνδεση / Αλλαγή )

Φωτογραφία Twitter

Σχολιάζετε χρησιμοποιώντας τον λογαριασμό Twitter. Αποσύνδεση / Αλλαγή )

Φωτογραφία Facebook

Σχολιάζετε χρησιμοποιώντας τον λογαριασμό Facebook. Αποσύνδεση / Αλλαγή )

Φωτογραφία Google+

Σχολιάζετε χρησιμοποιώντας τον λογαριασμό Google+. Αποσύνδεση / Αλλαγή )

Σύνδεση με %s