-
High-Resolution Building and Road Detection from Sentinel-2
Authors:
Wojciech Sirko,
Emmanuel Asiedu Brempong,
Juliana T. C. Marcos,
Abigail Annkah,
Abel Korme,
Mohammed Alewi Hassen,
Krishna Sapkota,
Tomer Shekel,
Abdoulaye Diack,
Sella Nevo,
Jason Hickey,
John Quinn
Abstract:
Map** buildings and roads automatically with remote sensing typically requires high-resolution imagery, which is expensive to obtain and often sparsely available. In this work we demonstrate how multiple 10 m resolution Sentinel-2 images can be used to generate 50 cm resolution building and road segmentation masks. This is done by training a `student' model with access to Sentinel-2 images to re…
▽ More
Map** buildings and roads automatically with remote sensing typically requires high-resolution imagery, which is expensive to obtain and often sparsely available. In this work we demonstrate how multiple 10 m resolution Sentinel-2 images can be used to generate 50 cm resolution building and road segmentation masks. This is done by training a `student' model with access to Sentinel-2 images to reproduce the predictions of a `teacher' model which has access to corresponding high-resolution imagery. While the predictions do not have all the fine detail of the teacher model, we find that we are able to retain much of the performance: for building segmentation we achieve 78.3% mIoU, compared to the high-resolution teacher model accuracy of 85.3% mIoU. We also describe a related method for counting individual buildings in a Sentinel-2 patch which achieves R^2 = 0.91 against true counts. This work opens up new possibilities for using freely available Sentinel-2 imagery for a range of tasks that previously could only be done with high-resolution satellite imagery.
△ Less
Submitted 20 June, 2024; v1 submitted 17 October, 2023;
originally announced October 2023.
-
Adding an Implication to Logics of Perfect Paradefinite Algebras
Authors:
Vitor Greati,
Sérgio Marcelino,
João Marcos,
Umberto Rivieccio
Abstract:
Perfect paradefinite algebras are De Morgan algebras expanded with an operation that allows for the full behavior of classical negation to be restored. They form a variety that is term-equivalent to the variety of involutive Stone algebras. Their associated multiple-conclusion (Set-Set) and single-conclusion (Set-Fmla) order-preserving logics are non-algebraizable self-extensional logics of formal…
▽ More
Perfect paradefinite algebras are De Morgan algebras expanded with an operation that allows for the full behavior of classical negation to be restored. They form a variety that is term-equivalent to the variety of involutive Stone algebras. Their associated multiple-conclusion (Set-Set) and single-conclusion (Set-Fmla) order-preserving logics are non-algebraizable self-extensional logics of formal inconsistency and undeterminedness determined by a six-valued matrix, studied in depth by Gomes et al. (2022) from both the algebraic and the proof-theoretical perspectives. In the present paper, we continue that study by investigating directions for conservatively expanding these logics with an implication connective (essentially, one that admits the deduction-detachment theorem). We first consider logics given by very simple and manageable non-deterministic semantics whose implication (in isolation) is classical. These, nevertheless, fail to be self-extensional. We then consider the implication realized by the relative pseudo-complement over the six-valued perfect paradefinite algebra. Our strategy is to expand the language of the latter algebra with this connective and study the (self-extensional) Set-Set and Set-Fmla order-preserving and top-assertional logics of the variety induced by the resulting algebra. We provide axiomatizations for such new variety and for such logics, drawing parallels with the class of symmetric Heyting algebras and with Moisil's 'symmetric modal logic'. For the Set-Set logic, in particular, the axiomatization we obtain is analytic. We close by studying interpolation properties for these logics and concluding that the new variety has the Maehara amalgamation property.
△ Less
Submitted 6 April, 2024; v1 submitted 13 September, 2023;
originally announced September 2023.
-
Proceedings 11th International Workshop on Theorem Proving Components for Educational Software
Authors:
Pedro Quaresma,
João Marcos,
Walther Neuper
Abstract:
The ThEdu series pursues the smooth transition from an intuitive way of doing mathematics at secondary school to a more formal approach to the subject in STEM education, while favouring software support for this transition by exploiting the power of theorem-proving technologies. What follows is a brief description of how the present volume contributes to this enterprise. The 11th International Wor…
▽ More
The ThEdu series pursues the smooth transition from an intuitive way of doing mathematics at secondary school to a more formal approach to the subject in STEM education, while favouring software support for this transition by exploiting the power of theorem-proving technologies. What follows is a brief description of how the present volume contributes to this enterprise. The 11th International Workshop on Theorem Proving Components for Educational Software (ThEdu'22), was a satellite event of the 8th Federated Logic Conference (FLoC 2022), July 31-August 12, 2022, Haifa, Israel ThEdu'22 was a vibrant workshop, with two invited talk by Thierry Dana-Picard (Jerusalem College of Technology, Jerusalem, Israel) and Yoni Zohar (Bar Ilan University, Tel Aviv, Israel) and four contributions. An open call for papers was then issued, and attracted seven submissions. Those submissions have been accepted by our reviewers, who jointly produced at least three careful reports on each of the contributions. The resulting revised papers are collected in the present volume. The contributions in this volume are a faithful representation of the wide spectrum of ThEdu, ranging from those more focused on the automated deduction research, not losing track of the possible applications in an educational setting, to those focused on the applications, in educational settings, of automated deduction tools and methods. We, the volume editors, hope that this collection of papers will further promote the development of theorem-proving based software, and that it will allow to improve the mutual understanding between computer scientists, mathematicians and stakeholders in education. While this volume goes to press, the next edition of the ThEdu workshop is being prepared: ThEdu'23 will be a satellite event of the 29th international Conference on Automated Deduction (CADE 2023), July 1-4, 2023, Rome, Italy.
△ Less
Submitted 9 March, 2023;
originally announced March 2023.
-
Finite two-dimensional proof systems for non-finitely axiomatizable logics
Authors:
Vitor Greati,
João Marcos
Abstract:
The characterizing properties of a proof-theoretical presentation of a given logic may hang on the choice of proof formalism, on the shape of the logical rules and of the sequents manipulated by a given proof system, on the underlying notion of consequence, and even on the expressiveness of its linguistic resources and on the logical framework into which it is embedded. Standard (one-dimensional)…
▽ More
The characterizing properties of a proof-theoretical presentation of a given logic may hang on the choice of proof formalism, on the shape of the logical rules and of the sequents manipulated by a given proof system, on the underlying notion of consequence, and even on the expressiveness of its linguistic resources and on the logical framework into which it is embedded. Standard (one-dimensional) logics determined by (non-deterministic) logical matrices are known to be axiomatizable by analytic and possibly finite proof systems as soon as they turn out to satisfy a certain constraint of sufficient expressiveness. In this paper we introduce a recipe for cooking up a two-dimensional logical matrix (or B-matrix) by the combination of two (possibly partial) non-deterministic logical matrices. We will show that such a combination may result in B-matrices satisfying the property of sufficient expressiveness, even when the input matrices are not sufficiently expressive in isolation, and we will use this result to show that one-dimensional logics that are not finitely axiomatizable may inhabit finitely axiomatizable two-dimensional logics, becoming, thus, finitely axiomatizable by the addition of an extra dimension. We will illustrate the said construction using a well-known logic of formal inconsistency called mCi. We will first prove that this logic is not finitely axiomatizable by a one-dimensional (generalized) Hilbert-style system. Then, taking advantage of a known 5-valued non-deterministic logical matrix for this logic, we will combine it with another one, conveniently chosen so as to give rise to a B-matrix that is axiomatized by a two-dimensional Hilbert-style system that is both finite and analytic.
△ Less
Submitted 18 May, 2022;
originally announced May 2022.
-
Proceedings 10th International Workshop on Theorem Proving Components for Educational Software
Authors:
João Marcos,
Walther Neuper,
Pedro Quaresma
Abstract:
This EPTCS volume contains the proceedings of the ThEdu'21 workshop, promoted on 11 July 2021, as a satellite event of CADE-28. Due to the COVID-19 pandemic, CADE-28 and all its co-located events happened as virtual events. ThEdu'21 was a vibrant workshop, with an invited talk by Gilles Dowek (ENS Paris-Saclay), eleven contributions, and one demonstration. After the workshop an open call for pape…
▽ More
This EPTCS volume contains the proceedings of the ThEdu'21 workshop, promoted on 11 July 2021, as a satellite event of CADE-28. Due to the COVID-19 pandemic, CADE-28 and all its co-located events happened as virtual events. ThEdu'21 was a vibrant workshop, with an invited talk by Gilles Dowek (ENS Paris-Saclay), eleven contributions, and one demonstration. After the workshop an open call for papers was issued and attracted 10 submissions, 7 of which have been accepted by the reviewers, and collected in the present post-proceedings volume.
The ThEdu series pursues the smooth transition from an intuitive way of doing mathematics at secondary school to a more formal approach to the subject in STEM education, while favouring software support for this transition by exploiting the power of theorem-proving technologies.
The volume editors hope that this collection of papers will further promote the development of theorem-proving based software, and that it will collaborate on improving mutual understanding between computer scientists, mathematicians and stakeholders in education.
△ Less
Submitted 2 February, 2022;
originally announced February 2022.
-
Proof Search on Bilateralist Judgments over Non-deterministic Semantics
Authors:
Vitor Greati,
Sérgio Marcelino,
João Marcos
Abstract:
The bilateralist approach to logical consequence maintains that judgments of different qualities should be taken into account in determining what-follows-from-what. We argue that such an approach may be actualized by a two-dimensional notion of entailment induced by semantic structures that also accommodate non-deterministic and partial interpretations, and propose a proof-theoretical apparatus to…
▽ More
The bilateralist approach to logical consequence maintains that judgments of different qualities should be taken into account in determining what-follows-from-what. We argue that such an approach may be actualized by a two-dimensional notion of entailment induced by semantic structures that also accommodate non-deterministic and partial interpretations, and propose a proof-theoretical apparatus to reason over bilateralist judgments using symmetrical two-dimensional analytical Hilbert-style calculi. We also provide a proof-search algorithm for finite analytic calculi that runs in at most exponential time, in general, and in polynomial time when only rules having at most one formula in the succedent are present in the concerned calculus.
△ Less
Submitted 17 July, 2021;
originally announced July 2021.
-
On Logics of Perfect Paradefinite Algebras
Authors:
Joel Gomes,
Vitor Greati,
Sérgio Marcelino,
João Marcos,
Umberto Rivieccio
Abstract:
The present study shows how to enrich De Morgan algebras with a perfection operator that allows one to express the Boolean properties of negation-consistency and negation-determinedness. The variety of perfect paradefinite algebras thus obtained (PP-algebras) is shown to be term-equivalent to the variety of involutive Stone algebras, introduced by R. Cignoli and M. Sagastume, and more recently stu…
▽ More
The present study shows how to enrich De Morgan algebras with a perfection operator that allows one to express the Boolean properties of negation-consistency and negation-determinedness. The variety of perfect paradefinite algebras thus obtained (PP-algebras) is shown to be term-equivalent to the variety of involutive Stone algebras, introduced by R. Cignoli and M. Sagastume, and more recently studied from a logical perspective by M. Figallo-L. Cantú and by S. Marcelino-U. Rivieccio. This equivalence plays an important role in the investigation of the 1-assertional logic and of the order-preserving logic associated to PP-algebras. The latter logic (here called PP<=) is characterized by a single 6-valued matrix and is shown to be a Logic of Formal Inconsistency and Formal Undeterminedness. We axiomatize PP<= by means of an analytic finite Hilbert-style calculus, and we present an axiomatization procedure that covers the logics corresponding to other classes of De Morgan algebras enriched by a perfection operator.
△ Less
Submitted 8 April, 2022; v1 submitted 17 June, 2021;
originally announced June 2021.
-
Proceedings 9th International Workshop on Theorem Proving Components for Educational Software
Authors:
Pedro Quaresma,
Walther Neuper,
João Marcos
Abstract:
The 9th International Workshop on Theorem-Proving Components for Educational Software (ThEdu'20) was scheduled to happen on June 29 as a satellite of the IJCAR-FSCD 2020 joint meeting, in Paris. The COVID-19 pandemic came by surprise, though, and the main conference was virtualised. Fearing that an online meeting would not allow our community to fully reproduce the usual face-to-face networking…
▽ More
The 9th International Workshop on Theorem-Proving Components for Educational Software (ThEdu'20) was scheduled to happen on June 29 as a satellite of the IJCAR-FSCD 2020 joint meeting, in Paris. The COVID-19 pandemic came by surprise, though, and the main conference was virtualised. Fearing that an online meeting would not allow our community to fully reproduce the usual face-to-face networking opportunities of the ThEdu initiative, the Steering Committee of ThEdu decided to cancel our workshop. Given that many of us had already planned and worked for that moment, we decided that ThEdu'20 could still live in the form of an EPTCS volume. The EPTCS concurred with us, recognising this very singular situation, and accepted our proposal of organising a special issue with papers submitted to ThEdu'20. An open call for papers was then issued, and attracted five submissions, all of which have been accepted by our reviewers, who produced three careful reports on each of the contributions. The resulting revised papers are collected in the present volume. We, the volume editors, hope that this collection of papers will help further promoting the development of theorem-proving-based software, and that it will collaborate to improve the mutual understanding between computer mathematicians and stakeholders in education. With some luck, we would actually expect that the very special circumstances set up by the worst sanitary crisis in a century will happen to reinforce the need for the application of certified components and of verification methods for the production of educational software that would be available even when the traditional on-site learning experiences turn out not to be recommendable.
△ Less
Submitted 27 October, 2020;
originally announced October 2020.
-
Proceedings 8th International Workshop on Theorem Proving Components for Educational Software
Authors:
Pedro Quaresma,
Walther Neuper,
João Marcos
Abstract:
This EPTCS volume contains the proceedings of the ThEdu'19 workshop, promoted on August 25, 2019, as a satellite event of CADE-27, in Natal, Brazil. Representing the eighth installment of the ThEdu series, ThEdu'19 was a vibrant workshop, with an invited talk by Sarah Winkler, four contributions, and the first edition of a Geometry Automated Provers Competition. After the workshop an open call f…
▽ More
This EPTCS volume contains the proceedings of the ThEdu'19 workshop, promoted on August 25, 2019, as a satellite event of CADE-27, in Natal, Brazil. Representing the eighth installment of the ThEdu series, ThEdu'19 was a vibrant workshop, with an invited talk by Sarah Winkler, four contributions, and the first edition of a Geometry Automated Provers Competition. After the workshop an open call for papers was issued and attracted seven submissions, six of which have been accepted by the reviewers, and collected in the present post-proceedings volume.
The ThEdu series pursues the smooth transition from an intuitive way of doing mathematics at secondary school to a more formal approach to the subject in STEM education, while favoring software support for this transition by exploiting the power of theorem-proving technologies.
The volume editors hope that this collection of papers will further promote the development of theorem-proving-based software, and that it will collaborate on improving mutual understanding between computer mathematicians and stakeholders in education.
△ Less
Submitted 26 February, 2020;
originally announced February 2020.
-
Combining fragments of classical logic: When are interaction principles needed?
Authors:
Carlos Caleiro,
Sérgio Marcelino,
João Marcos
Abstract:
We investigate the combination of fragments of classical logic as a way of conservatively extending a given Boolean logic by the addition of new connectives, and we precisely characterize the circumstances in which such a combination produces the corresponding fragment of classical logic over the signature containing connectives from both fragments given as input. If the thereby produced combined…
▽ More
We investigate the combination of fragments of classical logic as a way of conservatively extending a given Boolean logic by the addition of new connectives, and we precisely characterize the circumstances in which such a combination produces the corresponding fragment of classical logic over the signature containing connectives from both fragments given as input. If the thereby produced combined fragment is only incompletely characterized by the components given as input, this means that connectives from one component need to interact with connectives from the other component, giving rise to interaction principles. The main contributions strongly rely on the (well-known) description of the 2-valued clones made by Post, on the (not so well-known) axiomatization procedures for 2-valued matrices laid out by Rautenberg, and on Avron's non-deterministic matrices, which have (recently) been used to produce a significant advance on the understanding of the semantics of fibring.
△ Less
Submitted 16 October, 2018; v1 submitted 13 October, 2018;
originally announced October 2018.
-
Semi-BCI Algebras
Authors:
Regivan H. N. Santiago,
Benjamin Bedregal,
João Marcos,
Carlos Caleiro,
Jocivania Pinheiro
Abstract:
The notion of semi-BCI algebras is introduced and some of its properties are investigated. This algebra is another generalization for BCI-algebras. It arises from the "intervalization" of BCI algebras. Semi-BCI have a similar structure to Pseudo-BCI algebras however they are not the same. In this paper we also provide an investigation on the similarity between these classes of algebras by showing…
▽ More
The notion of semi-BCI algebras is introduced and some of its properties are investigated. This algebra is another generalization for BCI-algebras. It arises from the "intervalization" of BCI algebras. Semi-BCI have a similar structure to Pseudo-BCI algebras however they are not the same. In this paper we also provide an investigation on the similarity between these classes of algebras by showing how they relate to the process of intervalization.
△ Less
Submitted 13 March, 2018;
originally announced March 2018.
-
Merging fragments of classical logic
Authors:
Carlos Caleiro,
Sérgio Marcelino,
João Marcos
Abstract:
We investigate the possibility of extending the non-functionally complete logic of a collection of Boolean connectives by the addition of further Boolean connectives that make the resulting set of connectives functionally complete. More precisely, we will be interested in checking whether an axiomatization for Classical Propositional Logic may be produced by merging Hilbert-style calculi for two d…
▽ More
We investigate the possibility of extending the non-functionally complete logic of a collection of Boolean connectives by the addition of further Boolean connectives that make the resulting set of connectives functionally complete. More precisely, we will be interested in checking whether an axiomatization for Classical Propositional Logic may be produced by merging Hilbert-style calculi for two disjoint incomplete fragments of it. We will prove that the answer to that problem is a negative one, unless one of the components includes only top-like connectives.
△ Less
Submitted 27 June, 2017;
originally announced June 2017.
-
Sequent systems for negative modalities
Authors:
Ori Lahav,
João Marcos,
Yoni Zohar
Abstract:
Non-classical negations may fail to be contradictory-forming operators in more than one way, and they often fail also to respect fundamental meta-logical properties such as the replacement property. Such drawbacks are witnessed by intricate semantics and proof systems, whose philosophical interpretations and computational properties are found wanting. In this paper we investigate congruential non-…
▽ More
Non-classical negations may fail to be contradictory-forming operators in more than one way, and they often fail also to respect fundamental meta-logical properties such as the replacement property. Such drawbacks are witnessed by intricate semantics and proof systems, whose philosophical interpretations and computational properties are found wanting. In this paper we investigate congruential non-classical negations that live inside very natural systems of normal modal logics over complete distributive lattices; these logics are further enriched by adjustment connectives that may be used for handling reasoning under uncertainty caused by inconsistency or undeterminedness. Using such straightforward semantics, we study the classes of frames characterized by seriality, reflexivity, functionality, symmetry, transitivity, and some combinations thereof, and discuss what they reveal about sub-classical properties of negation. To the logics thereby characterized we apply a general mechanism that allows one to endow them with analytic ordinary sequent systems, most of which are even cut-free. We also investigate the exact circumstances that allow for classical negation to be explicitly defined inside our logics.
△ Less
Submitted 25 July, 2017; v1 submitted 15 June, 2017;
originally announced June 2017.
-
It ain't necessarily so: Basic sequent systems for negative modalities
Authors:
Ori Lahav,
João Marcos,
Yoni Zohar
Abstract:
We look at non-classical negations and their corresponding adjustment connectives from a modal viewpoint, over complete distributive lattices, and apply a very general mechanism in order to offer adequate analytic proof systems to logics that are based on them. Defining non-classical negations within usual modal semantics automatically allows one to treat equivalent formulas as synonymous, and to…
▽ More
We look at non-classical negations and their corresponding adjustment connectives from a modal viewpoint, over complete distributive lattices, and apply a very general mechanism in order to offer adequate analytic proof systems to logics that are based on them. Defining non-classical negations within usual modal semantics automatically allows one to treat equivalent formulas as synonymous, and to have a natural justification for a global version of the contraposition rule. From that perspective, our study offers a particularly useful environment in which negative modalities and their companions may be used for dealing with inconsistency and indeterminacy. After investigating modal logics based on arbitrary frames, we extend the results to serial frames, reflexive frames, functional frames, and symmetric frames. In each case we also investigate when and how classical negation may thereby be defined.
△ Less
Submitted 23 June, 2016; v1 submitted 13 June, 2016;
originally announced June 2016.
-
Cultural Anthropology through the Lens of Wikipedia: Historical Leader Networks, Gender Bias, and News-based Sentiment
Authors:
Peter A. Gloor,
Joao Marcos,
Patrick M. de Boer,
Hauke Fuehres,
Wei Lo,
Keiichi Nemoto
Abstract:
In this paper we study the differences in historical World View between Western and Eastern cultures, represented through the English, the Chinese, Japanese, and German Wikipedia. In particular, we analyze the historical networks of the World's leaders since the beginning of written history, comparing them in the different Wikipedias and assessing cultural chauvinism. We also identify the most inf…
▽ More
In this paper we study the differences in historical World View between Western and Eastern cultures, represented through the English, the Chinese, Japanese, and German Wikipedia. In particular, we analyze the historical networks of the World's leaders since the beginning of written history, comparing them in the different Wikipedias and assessing cultural chauvinism. We also identify the most influential female leaders of all times in the English, German, Spanish, and Portuguese Wikipedia. As an additional lens into the soul of a culture we compare top terms, sentiment, emotionality, and complexity of the English, Portuguese, Spanish, and German Wikinews.
△ Less
Submitted 31 July, 2015;
originally announced August 2015.
-
TryLogic tutorial: an approach to Learning Logic by proving and refuting
Authors:
Patrick Terrematte,
João Marcos
Abstract:
Aiming to offer a framework for blended learning to the teaching of proof theory, the present paper describes an interactive tutorial, called \textsc{TryLogic}, teaching how to solve logical conjectures either by proofs or refutations. The paper also describes the integration of our infrastructure with the Virtual Learning Environment \texttt{Moodle} through the IMS Learning Tools Interoperability…
▽ More
Aiming to offer a framework for blended learning to the teaching of proof theory, the present paper describes an interactive tutorial, called \textsc{TryLogic}, teaching how to solve logical conjectures either by proofs or refutations. The paper also describes the integration of our infrastructure with the Virtual Learning Environment \texttt{Moodle} through the IMS Learning Tools Interoperability specification, and evaluates the tool we have developed.
△ Less
Submitted 13 July, 2015;
originally announced July 2015.
-
Fail better: What formalized math can teach us about learning
Authors:
João Marcos
Abstract:
Real-life conjectures do not come with instructions saying whether they they should be proven or, instead, refuted. Yet, as we now know, in either case the final argument produced had better be not just convincing but actually verifiable in as much detail as our need for eliminating risk might require. For those who do not happen to have direct access to the realm of mathematical truths, the moder…
▽ More
Real-life conjectures do not come with instructions saying whether they they should be proven or, instead, refuted. Yet, as we now know, in either case the final argument produced had better be not just convincing but actually verifiable in as much detail as our need for eliminating risk might require. For those who do not happen to have direct access to the realm of mathematical truths, the modern field of formalized mathematics has quite a few lessons to contribute, and one might pay heed to what it has to say, for instance, about: the importance of employing proof strategies; the fine control of automation in unraveling the structure of a certain proof object; reasoning forward from the givens and backward from the goals, in develo** proof scripts; knowing when and how definitions and identities apply in a helpful way, and when they do not apply; seeing proofs [and refutations] as dynamical objects, not reflected by the static derivation trees that Proof Theory wants them to be. I believe that the great challenge for teachers and learners resides currently less on the availability of suitable generic tools than in combining them wisely in view of their preferred education paradigms and introducing them in a way that best fits their specific aims, possibly with the help of intelligent online interactive tutoring systems. As a proof of concept, a computerized proof assistant that makes use of several successful tools already freely available on the market and that takes into account some of the above findings about teaching and learning Logic is hereby introduced. To fully account for our informed intuitions on the subject it would seem that a little bit extra technology would still be inviting, but no major breakthrough is really needed: We are talking about tools that are already within our reach to develop, as the fruits of collaborative effort.
△ Less
Submitted 17 July, 2015; v1 submitted 13 July, 2015;
originally announced July 2015.
-
Bivalent semantics, generalized compositionality and analytic classic-like tableaux for finite-valued logics
Authors:
Carlos Caleiro,
João Marcos,
Marco Volpe
Abstract:
The paper is a contribution both to the theoretical foundations and to the actual construction of efficient automatizable proof procedures for non-classical logics. We focus here on the case of finite-valued logics, and exhibit: (i) a mechanism for producing a classic-like description of them in terms of an effective variety of bivalent semantics; (ii) a mechanism for extracting, from the bivalent…
▽ More
The paper is a contribution both to the theoretical foundations and to the actual construction of efficient automatizable proof procedures for non-classical logics. We focus here on the case of finite-valued logics, and exhibit: (i) a mechanism for producing a classic-like description of them in terms of an effective variety of bivalent semantics; (ii) a mechanism for extracting, from the bivalent semantics so obtained, uniform (classically-labeled) cut-free standard analytic tableaux with possibly branching invertible rules and paired with proof strategies designed to guarantee termination of the associated proof procedure; (iii) a mechanism to also provide, for the same logics, uniform cut-based tableau systems with linear rules. The latter tableau systems are shown to be adequate even when restricted to analytic cuts, and they are also shown to polynomially simulate truth-tables, a feature that is not enjoyed by the former standard type of tableau systems (not even in the 2-valued case). The results are based on useful generalizations of the notions of analyticity and compositionality, and illustrate a theory that applies to many other classes of non-classical logics.
△ Less
Submitted 16 August, 2014;
originally announced August 2014.
-
Clausal Resolution for Modal Logics of Confluence
Authors:
Cláudia Nalon,
João Marcos,
Clare Dixon
Abstract:
We present a clausal resolution-based method for normal multimodal logics of confluence, whose Kripke semantics are based on frames characterised by appropriate instances of the Church-Rosser property. Here we restrict attention to eight families of such logics. We show how the inference rules related to the normal logics of confluence can be systematically obtained from the parametrised axioms th…
▽ More
We present a clausal resolution-based method for normal multimodal logics of confluence, whose Kripke semantics are based on frames characterised by appropriate instances of the Church-Rosser property. Here we restrict attention to eight families of such logics. We show how the inference rules related to the normal logics of confluence can be systematically obtained from the parametrised axioms that characterise such systems. We discuss soundness, completeness, and termination of the method. In particular, completeness can be modularly proved by showing that the conclusions of each newly added inference rule ensures that the corresponding conditions on frames hold. Some examples are given in order to illustrate the use of the method.
△ Less
Submitted 1 May, 2014;
originally announced May 2014.
-
On Achievable Rates of the Two-user Symmetric Gaussian Interference Channel
Authors:
Omar Mehanna,
John Marcos,
Nihar **dal
Abstract:
We study the Han-Kobayashi (HK) achievable sum rate for the two-user symmetric Gaussian interference channel. We find the optimal power split ratio between the common and private messages (assuming no time-sharing), and derive a closed form expression for the corresponding sum rate. This provides a finer understanding of the achievable HK sum rate, and allows for precise comparisons between this s…
▽ More
We study the Han-Kobayashi (HK) achievable sum rate for the two-user symmetric Gaussian interference channel. We find the optimal power split ratio between the common and private messages (assuming no time-sharing), and derive a closed form expression for the corresponding sum rate. This provides a finer understanding of the achievable HK sum rate, and allows for precise comparisons between this sum rate and that of orthogonal signaling. One surprising finding is that despite the fact that the channel is symmetric, allowing for asymmetric power split ratio at both users (i.e., asymmetric rates) can improve the sum rate significantly. Considering the high SNR regime, we specify the interference channel value above which the sum rate achieved using asymmetric power splitting outperforms the symmetric case.
△ Less
Submitted 12 October, 2010;
originally announced October 2010.
-
Automatic Generation of Proof Tactics for Finite-Valued Logics
Authors:
João Marcos
Abstract:
A number of flexible tactic-based logical frameworks are nowadays available that can implement a wide range of mathematical theories using a common higher-order metalanguage. Used as proof assistants, one of the advantages of such powerful systems resides in their responsiveness to extensibility of their reasoning capabilities, being designed over rule-based programming languages that allow the us…
▽ More
A number of flexible tactic-based logical frameworks are nowadays available that can implement a wide range of mathematical theories using a common higher-order metalanguage. Used as proof assistants, one of the advantages of such powerful systems resides in their responsiveness to extensibility of their reasoning capabilities, being designed over rule-based programming languages that allow the user to build her own `programs to construct proofs' - the so-called proof tactics.
The present contribution discusses the implementation of an algorithm that generates sound and complete tableau systems for a very inclusive class of sufficiently expressive finite-valued propositional logics, and then illustrates some of the challenges and difficulties related to the algorithmic formation of automated theorem proving tactics for such logics. The procedure on whose implementation we will report is based on a generalized notion of analyticity of proof systems that is intended to guarantee termination of the corresponding automated tactics on what concerns theoremhood in our targeted logics.
△ Less
Submitted 25 March, 2010;
originally announced March 2010.
