1,720,981 research outputs found
Proof verification within set theory
Full text linkThe proof-checker ÆtnaNova, aka Ref, processes proof scenarios to establish whether or not they are formally correct. A scenario, typically written by a working mathematician or computer scientist, consists of definitions, theorem statements and proofs of the theorems. There is a construct enabling one to package definitions and theorems into reusable proofware components. The deductive system underlying Ref mainly first-order, but with an important second-order feature: the packaging construct just mentioned is a variant of the Zermelo-Fraenkel set theory, ZFC, with axioms of regularity and global choice. This is apparent from the very syntax of the language, borrowing from the set-theoretic tradition many constructs, e.g. abstraction terms. Much of Ref’s naturalness, comprehensiveness, and readability, stems from this foundation; much of its effectiveness, from the fifteen or so built-in mechanisms, tailored on ZFC, which constitute its inferential armory. Rather peculiar aspects of Ref, in comparison to other proof-assistants (Mizar to mention one), are that Ref relies only marginally on predicate calculus and that types play no significant role, in it, as a foundation.
This talk illustrates the state-of-the-art of proof-verification technology based on set theory, by reporting on ‘proof-pearl’ scenarios currently under development and by examining some small-scale, yet significant, examples of use of Ref. The choice of examples will reflect today’s tendency to bring Ref’s scenarios closer to algorithm-correctness verification, mainly referred to graphs. The infinity axiom rarely plays a role in applications to algorithms; nevertheless the availability of all resources of ZFC is important in general: for example, relatively unsophisticated argumentations enter into the proof that the Davis-Putnam-Logemann-Loveland satisfiability test is correct, but in order to prove the compactness of propositional logic or Stone’s representation theorem for Boolean algebras one can fruitfully resort to Zorn’s lemma
A proof-checking experiment on representing graphs as membership digraphs
No full textWe developed, and computer-checked by means of the Ref verifier, a formal proof that every weakly extensional, acyclic (finite) digraph can be decorated injectively a` la Mostowski by finite sets so that its arcs mimic membership. We managed to have one sink decorated with ∅ by this injection.
We likewise proved that a graph whatsoever admits a weakly extensional and acyclic orientation; consequently, and in view of what precedes, one can regard its edges as membership arcs, each deprived of the direction assigned to it by the orientation.
These results will be enhanced in a forthcoming scenario, where every connected claw-free graph G will receive an extensional acyclic orientation and will, through such an orientation, be represented as a transitive set T so that the membership arcs between members of T will correspond to the edges of G
Encodings of Sets and Hypersets
No full textWe will present some results and open problems on an extension of the Ackermann encoding of Hereditarily Finite Sets into Natural Numbers. In particular, we will introduce and discuss a simple modification of the above mentioned Ackermann encoding, that should naturally generalize from Hereditarily Finite Sets to Hereditarily Finite Hypersets
On model-based reasoning: recent trends and current developments
Full text linkProofs and models are the mainstay of automated reasoning. Traditionally, proofs have taken center stage, because in first-order logic theorem proving is semi-decidable, and model building is not. The growth of algorithmic reasoning and of its applications to software has changed the balance, because if satisfiability is decidable, symmetry is restored, and models are useful for applications and intuitive for users
A Description Logics Tableau Reasoner in Prolog
No full textDescription Logics (DLs) are gaining a widespread adoption
as the popularity of the Semantic Web increases. Traditionally, reasoning algorithms for DLs have been implemented in procedural languages such as Java or C++. In this paper, we present the system TRILL for \Tableau
Reasoner for descrIption Logics in proLog". TRILL answers queries to SHOIN(D) knowledge bases using a tableau algorithm. Prolog nondeterminism is used for easily handling non-deterministic expansion rules that produce more than one tableau. Moreover, given a query, TRILL is
able to return instantiated explanations for the query, i.e., instantiated minimal sets of axioms that allow the entailment of the query. The Thea2 library is exploited by TRILL for parsing ontologies and for the internal
Prolog representation of DL axioms
Proceedings of the fourth edition of the International Workshop on Semantic Web and Ontology Design for Cultural Heritage (SWODCH 2024. Semantic Web and Ontology Design for Cultural Heritage 2024)
No full textInternational audienceTable of Contents— Preface— Towards an Annotation Data Model for a Scholarly Semantic Annotation Platform in Visual Heritage: A Case Study Using the Murten Panorama / Tsz Kin Chau, Daniel Jaquet, Sarah Kenderdine— An OWL Ontology for Linguistic Phenomena with Applications to Gallo-Italic Dialects in Sicily / Domenico Cantone, Vincenzo Nicolò Di Caro, Cristiano Longo, Salvatore Menza, Marianna Nicolosi Asmundo, Daniele Francesco Santamaria— Operationalizing Scholarly Observations in OWL / Emilio M. Sanfilippo, Claudio Masolo, Alessandro Mosca, Gaia Tomazzoli— Assessing the Expressivity of Iconclass to Embody Emotional Features in Classical Iconography / Alessandro Adamou, Davide Picca— Ontological Patterns for Modeling the Validity of Spatiotemporal Statements / Nicola Carboni— Spatio-Temporal Reasoning on Stratigraphic Data in Archaeology: Formalization of the Harris Laws as Inferences Using CIDOC CRM / Anaïs Guillem, Muriel van Ruymbeke, Øyvind Eide, Livio de Luca— Graphing Trees: The Nodes and Edges of Nabokov’s Worlds / Shakeeb Arzoo, Aidan Hogan, Stephen H. Blackwel
Proceedings of the fourth edition of the International Workshop on Semantic Web and Ontology Design for Cultural Heritage (SWODCH 2024. Semantic Web and Ontology Design for Cultural Heritage 2024)
No full textInternational audienceTable of Contents— Preface— Towards an Annotation Data Model for a Scholarly Semantic Annotation Platform in Visual Heritage: A Case Study Using the Murten Panorama / Tsz Kin Chau, Daniel Jaquet, Sarah Kenderdine— An OWL Ontology for Linguistic Phenomena with Applications to Gallo-Italic Dialects in Sicily / Domenico Cantone, Vincenzo Nicolò Di Caro, Cristiano Longo, Salvatore Menza, Marianna Nicolosi Asmundo, Daniele Francesco Santamaria— Operationalizing Scholarly Observations in OWL / Emilio M. Sanfilippo, Claudio Masolo, Alessandro Mosca, Gaia Tomazzoli— Assessing the Expressivity of Iconclass to Embody Emotional Features in Classical Iconography / Alessandro Adamou, Davide Picca— Ontological Patterns for Modeling the Validity of Spatiotemporal Statements / Nicola Carboni— Spatio-Temporal Reasoning on Stratigraphic Data in Archaeology: Formalization of the Harris Laws as Inferences Using CIDOC CRM / Anaïs Guillem, Muriel van Ruymbeke, Øyvind Eide, Livio de Luca— Graphing Trees: The Nodes and Edges of Nabokov’s Worlds / Shakeeb Arzoo, Aidan Hogan, Stephen H. Blackwel
- …
