Using conditional trace slicing for improving Maude programs
- Alpuente Frasnedo, María; BALLIS, DEMIS; Frechina, F.; ROMERO, DANIEL OMAR
Understanding the behavior of software is important for the existing software to be improved. In this paper, we present a trace slicing technique that is suitable for analyzing complex, textually-large computations in rewriting logic, which is a general framework efficiently implemented in the Maude language that seamlessly unifies a wide variety of logics and models of concurrency. Given a Maude execution trace T and a slicing criterion for the trace (i.e., a piece of information that we want to observe in the final computation state), we traverse T from back to front and the backward dependence of the observed information...
Un estudio sobre la premisa mayor del silogismo cosmológico kantiano
- Herszenbaun, Miguel Alejandro
The relationship between the logical maxim and the synthetic principle of pure reason (A 307-308/B 364-365) plays an important role in the "Transcendental Dialectic". This is apparent by noting that the formulation of the problems treated in the Dialectic has an explicit reference to the transition from the maxim to the principle (A 308-309/B 365-366). Nevertheless, Kant doesn't explain how this transition is made. I intend to explain this transition through a detailed study of the major premise of the cosmological syllogism, where it has an important role. I claim that this passage is understandable only by assuming a restricted...
Acerca del ámbito de investigación de la lógica informal
- Behnisch, Cristina Helena
En los trabajos publicados bajo el título general de ‘Lógica informal’ a lo largo de las últimas décadas es admitida la ausencia de una teoría con un grado generalizado de aceptación; lo mismo ocurre con respecto a la metodología. Bajo la hipótesis de que bajo estas circunstancias sería oportuno contar con alguna precisión en lo que se refiere al objetivo principal de la investigación, examinaré algunas caracterizaciones de la lógica informal que aparecen en artículos especializados recientes. Me orienta el propósito de reconocer el ámbito de la problemática bajo estudio, sobre la base de algún criterio que dé cuenta, en...
Algoritmos para el tratamiento y selección de productos financieros en la incertidumbre
- Vizuete Luciano, Emilio
La tesis doctoral realizada tiene como principal objetivo desarrollar nuevas aplicaciones y modelos dentro de la Matemática del Azar y la Incertidumbre; con la finalidad de facilitar al sujeto decisor su elección en un entorno tan inseguro, incierto y cambiante como en el que nos encontramos en el Siglo XXI.
La investigación realizada ha tenido como objetivos específicos:
1. Llevar a cabo un profundo estudio sobre las aportaciones realizadas por la Comunidad Científica en la Web of Science (WOS).
2. Estudiar los aspectos introductorios y generales que se han realizado hasta la fecha en el campo de la lógica borrosa dentro del ámbito del objetivo...
Abstract Certification of Global Non-Interference in Rewriting Logic ⋆
- Mauricio Alba-castro; María Alpuente; Santiago Escobar
Abstract. Non–interference is a semantic program property that assigns confidentiality levels to data objects and prevents illicit information flows from occurring from high to low security levels. In this paper, we present a novel security model for global non–interference which approximates non–interference as a safety property. We also propose a certification technique for global non-interference of complete Java classes based on rewriting logic, a very general logical and semantic framework that is efficiently implemented in the high-level programming language Maude. Starting from an existing Java semantics specification written in Maude, we develop an extended, information–flow Java semantics that allows us...
Automated certification of non-interference in rewriting logic
- Mauricio Alba-castro; María Alpuente; Santiago Escobar
Abstract. In this paper we propose a certification technique for noninterference of Java programs based on rewriting logic, a very general logical and semantic framework efficiently implemented in the high-level programming language Maude. Non–interference is a semantic program property that prevents illicit information flow to happen. Starting from a basic specification of the semantics of Java written in Maude, we develop an information–flow extension of this operational Java semantics which allows us to observe non-interference of Java programs. Then we develop in Maude an abstract, finite-state version of the information-flow operational semantics which supports finite program verification. As a by–product...
Looking for P Truth
- Andrés Cordón-franco; Miguel Angel Gutiérrez-naranjo; Mario J. Pérez-jiménez
Abstract. In a general sense, Logic studies how to derive new pieces of information from previous ones. In this paper we explore the analogies between P systems, where new configurations can be obtained from previous ones by using a set of rules, and the derivation of new theorems from previous ones or from axioms by using inference rules. 1
Without aspiring to historical or systematic completeness, this paper presents an informal survey of some lines in 20 th century Polish logic, together with some general historical background, and making special reference to the author’s environment in Opole, and the contributions by her teacher Jerzy Słupecki. Further published material can be found in the appended bibliography. 2 Contents Preface (Johan van Benthem)……………………………………………………………… … 3 POLISH LOGIC, a few lines from a personal perspective…………………………………….4
Logic and Meaning of Programs General Terms Theory
- Rémy Haemmerlé; Pedro Lopez-garcia; Manuel V. Hermenegildo
This paper introduces and studies the notion of CLP projection for Constraint Handling Rules (CHR). The CLP projection consists of a naive translation of CHR programs into Constraint Logic Programs (CLP). We show that the CLP projection provides a safe operational and declarative approximation for CHR programs. We demonstrate moreover that a confluent CHR program has a least model, which is precisely equal to the least model of its CLP projection (closing hence a ten year-old conjecture by Abdenader et al.). Finally, we illustrate how the notion of CLP projection can be used in practice to apply CLP analyzers to...
Fine’s Theorem on First-Order Complete Modal Logics
- Robert Goldblatt
Fine’s Canonicity Theorem states that if a modal logic is determined by a first-order definable class of Kripke frames, then it is valid in its canonical frames. This article reviews the background and context of this result, and the history of its influence on further research. It then develops a new characterisation of when a logic is canonically valid, providing a precise point of distinction with the property of firstorder completeness. 1 The Canonicity Theorem and Its Impact In his PhD research, completed in 1969, and over the next half-dozen years, Kit Fine made a series of fundamental contributions to...
Logic, Mathematics, and General Agency
- Johan Van Benthem
If logic is the general study of a priori valid reasoning, then where is the paradigmatic area where we see this reasoning in its full glory? To some, this is clearly mathematics, where precision is relentless, and strings of inferences are taken to impressive lengths. But on another view, the highest form of reasoning is displayed in the ordinary world of common sense – say, when engaging in conversation about something that matters, where pure information is deeply intertwined with evaluation and goals, and where, crucially, we are surrounded by further agents like us that we must interact with. On...
The HOL System DESCRIPTION Preface
This volume contains the description of the HOL system. making up the documentation for HOL: It is one of four volumes (i) LOGIC: a formal description of the higher order logic implemented by the HOL system. (ii) TUTORIAL: a tutorial introduction to HOL, with case studies. (iii) DESCRIPTION: a detailed user’s guide for the HOL system; (iv) REFERENCE: the reference manual for HOL. These four documents will be referred to by the short names (in small slanted capitals) given above. This document, DESCRIPTION, is an advanced guide for users with some prior experience of the system. Beginners should start with...
Step-Indexed Normalization for a Language with General Recursion
- Chris Casinghino; Vilhelm Sjöberg; Stephanie Weirich
The TRELLYS project has produced several designs for practical dependently typed languages. These languages are broken into two fragments—a logical fragment where every term normalizes and which is consistent when interpreted as a logic, and a programmatic fragment with general recursion and other convenient but unsound features. In this paper, we present a small example language in this style. Our design allows the programmer to explicitly mention and pass information between the two fragments. We show that this feature substantially complicates the metatheory and present a new technique, combining the traditional Girard–Tait method with step-indexed logical relations, which we use...
Declarative PTIME Queries to Relational Databases
- Patrick Doherty; Witold Lukaszewicz; Andrzej Sza Las; Patrick Doherty; Witold Lukaszewicz; Andrzej Sza
In this paper, we consider the problem of expressing and computing PTIME queries to relational deductive databases in a purely declarative query language, SHQL (Semi-Horn Query Language). Assuming the relational databases in question are ordered, we showthat all SHQL queries are computable in PTIME and the whole class of PTIME queries is expressible in SHQL. Although similar results have been proven for xpoint languages and extensions to datalog, the claim is that SHQL has the advantage of being purely declarative, where the negation operator is interpreted as classical negation, mixed quanti ers may be used and a query is simply...
Declarative PTIME Queries to Relational Databases
- Patrick Doherty; Witold Lukaszewicz; Andrzej Sza
In this paper, we consider the problem of expressing and computing PTIME queries to relational deductive databases in a purely declarative query language we introduce, called SHQL (Semi-Horn Query Language). Assuming the relational databases in question are ordered, we show that all SHQL queries are computable in PTIME and the whole class of PTIME queries is expressible in SHQL. Although similar results have been proven for xpoint languages and extensions to datalog, the claim is that SHQL has the advantage of being purely declarative, where the negation operator is interpreted as classical negation, mixed quanti ers may be used and...
Magically Constraining the Inverse Method with Dynamic Polarity Assignment 3:
- Kaustuv Chaudhuri
Abstract. Given a logic program that is terminating and mode-correct in an idealised Prolog interpreter (i.e., in a top-down logic programming engine), a bottom-up logic programming engine can be used to compute exactly the same set of answers as the top-down engine for a given mode-correct query by rewriting the program and the query using the Magic Sets Transformation (MST). In previous work, we have shown that focusing can logically characterise the standard notion of bottom-up logic programming if atomic formulas are statically given a certain polarity assignment. In an analogous manner, dynamically assigning polarities can characterise the effect of...
Reasoning about quantum systems
- P. Mateus; A. Sernadas
Abstract. A new logic is proposed for reasoning about quantum systems. The logic embodies the postulates of quantum physics and it was designed from the semantics upwards by identifying quantum models with superpositions of classical models. This novel approach to quantum logic is completely different from the traditional approach of Birkhoff and von Neumann. It has the advantage of making quantum logic an extension of classical logic. The key new ingredient of the language of the proposed logic is a rather general modal operator. The logic incorporates probabilistic reasoning (in the style of Nilsson) in order to deal with uncertainty...
Using Prediction to Accelerate Coherence Protocols
Most large shared-memory multiprocessors use directory protocols to keep per-processor caches coherent. Some memory references in such systems, however, suffer long latencies for misses to remotelycached blocks. To ameliorate this latency, researchers have augmented standard coherence protocols with optimizations for specific sharing patterns, such as read-modify-write, producer-consumer, and migratory sharing. This paper seeks to replace these directed solutions with general prediction logic that monitors coherence activity and triggers appropriate coherence actions. This paper takes the first step toward using general prediction to accelerate coherence protocols by developing and evaluating the Cosmos coherence message predictor. Cosmos predicts the source and type...
PRISM User’s Manual (Version 2.0.3)
- Taisuke Sato; Neng-fa Zhou; Yoshitaka Kameya; Yusuke Izumi; Yoshitaka Kameya; Yusuke Izumi Preface
The past several years have witnessed a tremendous interest in logic-based probabilistic learning as testified by the number of formalisms and systems and their applications. Logic-based probabilistic learning is a multidisciplinary research area that integrates relational or logic formalisms, probabilistic reasoning mechanisms, and machine learning and data mining principles. Logic-based probabilistic learning has found its way into many application areas including bioinformatics, diagnosis and troubleshooting, stochastic language processing, information retrieval, linkage analysis and discovery, robot control, and probabilistic constraint solving. PRISM (PRogramming In Statistical Modeling) is a logic-based language that integrates logic programming and probabilistic reasoning including parameter learning. It...
Fictional Separation Logic
- Jonas Braband Jensen; Lars Birkedal
Separation logic formalizes the idea of local reasoning for heap-manipulating programs via the frame rule and the separating conjunction P ∗ Q, which describes states that can be split into separate parts, with one satisfying P and the other satisfying Q. In standard separation logic, separation means physical separation. In this paper, we introduce fictional separation logic, which includes more general forms of fictional separating conjunctions P ∗ Q, where ∗ does not require physical separation, but may also be used in situations where the memory resources described by P and Q overlap. We demonstrate, via a range of examples,...