arXiv subjects

João Marcos

Publications and source records attributed to João Marcos.

24 records · Page 2Linked to original sources

arXiv2016

It ain't necessarily so: Basic sequent systems for negative modalities

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.

cs.LO↗

arXiv2015

Fail better: What formalized math can teach us about learning

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 developing 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.

cs.CY↗

arXiv2015

TryLogic tutorial: an approach to Learning Logic by proving and refuting

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.

cs.CY↗

arXiv2014

Bivalent semantics, generalized compositionality and analytic classic-like tableaux for finite-valued logics

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.

cs.LO↗

arXiv2014

Clausal Resolution for Modal Logics of Confluence

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.

cs.LO↗

arXiv2010

Automatic Generation of Proof Tactics for Finite-Valued Logics

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.

cs.LO↗