Argumentation and rule-based logic in mathematical proving and legal artificial intelligence applications

Abstract

Proving is the validation of conclusions by application of logical arguments and rules to assumptions. In mathematics, an assertion is not accepted as true or valid unless it is accompanied by a proof. However, proving processes do not exist only in mathematics, but almost everywhere — in the physical sciences, in computer science, in legal and ethical argumentation, in philosophy, and so on. During the proving process, a dialogue between agents is required to clarify obscure inference steps, fill gaps, or reveal implicit assumptions in a purported proof. Hence, argumentation is an integral component of the discovery process of proofs in general but also — more specifically — in mathematical proofs. The first part of this thesis presents how logic-based argumentation theories can be applied to describe specific features in the development of proof-events, highlighting the relation between formal proof, informal human reasoning, cognitive processes, and social interactions. The concept of proof-event was coined by Goguen who described mathematical proof as a social event that takes place in space and time, designed to cover not only “traditional” formal proofs but all kinds of proofs including incomplete or purported proofs. In real-life cognitive processes, informal human reasoning and social aspects play a significant role. Our approach attempts to make proof-events more comprehensive to express the complete trajectory of a mathematical proofevent, including formal and informal proving steps, until the ultimate validation of the proving outcome. Thus, we present an extended version of proof-event calculus named Argumentation-based Proof-Event Calculus (APEC) which is built on the argumentation theories of Pollock, Toulmin, and Kakas designed to capture the internal and external structure of a collaborative mathematical practice. The second part of this thesis demonstrates two scopes of implementation to highlight the applicability and the expressivity of logic-based approaches in real-life proving scenarios. The first scope concerns explicit mathematical proving practices, which can be applied for an in-depth analysis of the internal steps in a mathematical proof, as indicated in the paradigm of Zero Knowledge Proofs, or for modeling a more external perspective to highlight the social interactions and the progress during a multi-agent proving process, as illustrated in the cases of Mini-Polymath 4 project and Fermat’s Last Theorem. The second scope is for implicit proving processes encoded in legal and ethical aspects of medical devices and wearable robots. Legal-AI models in the medical sector are presented through logic-based systems, where a legal text is represented by rules that can express legal arguments and exceptions and can provide explanations as audit trails of how a particular conclusion was proved. The logic-based legal systems presented in this work are: the WeaRED, an ethical decision-making system on Wearable Robots’ data privacy; the AMeDC and the Medical Devices Rules systems regarding Medical Devices Regulation; and the ExosCE Rules system regarding the regulation of exoskeletons.

Απόδειξη είναι η επικύρωση συμπερασμάτων με την εφαρμογή λογικών επιχειρημάτων και κανόνων σε υποθέσεις. Στα μαθηματικά, ένας ισχυρισμός για να γίνει δεκτός ως αληθής ή έγκυρος πρέπει να συνοδεύεται από απόδειξη. Ωστόσο, αποδεικτικές διαδικασίες δεν υπάρχουν μόνο στα μαθηματικά, αλλά σχεδόν παντού – στις φυσικές επιστήμες, στην επιστήμη των υπολογιστών, στη νομική και ηθική επιχειρηματολογία, στη φιλοσοφία και ούτω καθεξής. Κατά τη διάρκεια της αποδεικτικής διαδικασίας, απαιτείται διάλογος μεταξύ των δρώντων (agents) για να διευκρινιστούν τα ασαφή βήματα, να καλυφθούν κενά ή να αποδειχθούν έμμεσες υποθέσεις σε μια μη ολοκληρωμένη απόδειξη. Κατά συνέπεια, η επιχειρηματολογία είναι αναπόσπαστο συστατικό της διαδικασίας ανακάλυψης των αποδείξεων γενικότερα αλλά και –πιο συγκεκριμένα– στις μαθηματικές αποδείξεις. Το πρώτο σκέλος της εργασίας παρουσιάζει πώς οι θεωρίες επιχειρηματολογίας που βασίζονται στη λογική μπορούν να εφαρμοστούν για να περιγράψουν συγκεκριμένα χαρακτηριστικά στην ανάπτυξη των αποδεικτικών συμβάντων (proof-event), τονίζοντας τη σχέση μεταξύ επίσημης απόδειξης, άτυπου ανθρώπινου συλλογισμού, γνωστικών διαδικασιών και κοινωνικών αλληλεπιδράσεων. Η έννοια του αποδεικτικού συμβάντος επινοήθηκε από τον Goguen, ο οποίος περιέγραψε τη μαθηματική απόδειξη ως ένα κοινωνικό γεγονός που λαμβάνει χώρα σε συγκεκριμένο χώρο και χρόνο, σχεδιασμένο να καλύπτει όχι μόνο τις «παραδοσιακές» τυπικές αποδείξεις αλλά όλα τα είδη αποδείξεων, συμπεριλαμβανομένων των ελλιπών ή υποθετικών αποδείξεων. Στις πραγματικές γνωστικές διαδικασίες, ο άτυπος ανθρώπινος συλλογισμός και οι κοινωνικές πτυχές παίζουν σημαντικό ρόλο. Η προσέγγισή μας επιχειρεί να κάνει τα αποδεικτικά συμβάντα πιο περιεκτικά για να εκφράσει την πλήρη τροχιά μιας μαθηματικής διαδικασίας, συμπεριλαμβανομένων τόσο των τυπικών όσο και των άτυπων βημάτων απόδειξης, μέχρι την τελική επικύρωση του αποτελέσματος της απόδειξης. ΄Ετσι, παρουσιάζουμε μια εκτεταμένη εκδοχή του λογισμού αποδεικτικών συμβάντων με το όνομα Argumentation-based ProofEvent Calculus (APEC), η οποία βασίζεται σε θεωρίες επιχειρηματολογίας των Pollock, Toulmin και Kakas που έχουν σχεδιαστεί για να μπορούν να καταγράφουν την εσωτερική και εξωτερική δομή μιας συνεργατικής μαθηματικής πρακτικής. Στο δεύτερο σκέλος της εργασίας παρουσιάζονται δύο πεδία εφαρμογής για να τονιστεί η αποτελεσματικότητα και η εκφραστικότητα των βασισμένων στη λογική προσεγγίσεων σε πραγματικά σενάρια αποδεικτικών διαδικασιών. Το πρώτο πεδίο αφορά άμεσες πρακτικές μαθηματικής απόδειξης που μπορούν να εφαρμοστούν είτε για μια εις βάθος ανάλυση των εσωτερικών βημάτων σε μια μαθηματική απόδειξη, όπως υποδεικνύεται στο παράδειγμα των Zero Knowledge Proofs, είτε για τη μοντελοποίηση μιας πιο εξωτερικής προοπτικής για την ανάδειξη των κοινωνικών αλληλεπιδράσεων και της εξέλιξης κατά τη διάρκεια μιας διαδικασίας απόδειξης πολλών δρώντων, όπως απεικονίζεται στα παραδείγματα του Mini-Polymath 4 πρότζεκτ και του Τελευταίου Θεωρήματος του Φερμά. Το δεύτερο πεδίο αφορά έμμεσες διαδικασίες απόδειξης που αναφέρονται σε ηθικές και νομικές πτυχές των ιατρικών συσκευών και των φορητών ρομπότ (wearable robots). Τα νομικά μοντέλα τεχνητής νοημοσύνης στον ιατρικό τομέα μπορούν να εκφραστούν αποτελεσματικά μέσω συστημάτων που βασίζονται στη λογική, όπου ένα νομικό κείμενο περιγράφεται από κανόνες που μπορούν να εκφράσουν νομικά επιχειρήματα και εξαιρέ- σεις και μπορούν να ελεγχθούν και να παράσχουν επεξηγήσεις για το πώς αποδείχθηκε ένα συγκεκριμένο συμπέρασμα. Τα συστήματα με βάση τη λογική που παρουσιάζονται σε αυτήν την εργασία είναι: το WeaRED, ένα σύστημα ηθικής λήψης αποφάσεων σχετικά με το απόρρητο των προσωπικών δεδομένων των Wearable Robots, τα συστήματα AMeDC και Medical Devices Rules σχετικά με τη νομοθεσία για τα ιατροτεχνολογικά προϊόντα, και το σύστημα ExosCE σχετικά με το νομικό καθεστώς των εξωσκελετών.