Página 1 dos resultados de 1256 itens digitais encontrados em 0.021 segundos

## A Logic and tool for local reasoning about security protocols

Toninho, Bernardo Parente Coutinho Fernandes
Fonte: FCT - UNL Publicador: FCT - UNL
Relevância na Pesquisa
46.07%
Trabalho apresentado no âmbito do Mestrado em Engenharia Informática, como requisito parcial para obtenção do grau de Mestre em Engenharia Informática; This thesis tackles the problem of developing a formal logic and associated model-checking techniques to verify security properties, and its integration in the Spatial Logic Model Checker(SLMC) tool. In the areas of distributed system design and analysis, there exists a substantial amount of work related to the verification of correctness properties of systems, in which the work aimed at the verification of security properties mostly relies on precise yet informal methods of reasoning. This work follows a line of research that applies formal methodologies to the verification of security properties in distributed systems, using formal tools originally developed for the study of concurrent and distributed systems in general. Over the years, several authors have proposed spatial logics for local and compositional reasoning about algebraic models of distributed systems known as process calculi. In this work, we present a simplification of a process calculus known as the Applied - calculus, introduced by Abadi and Fournet, designed for the study of security protocols. We then develop a spatial logic for this calculus...

## Mathematical Logic in the Human Brain: Semantics

Friedrich, Roland M.; Friederici, Angela D.
Fonte: Public Library of Science Publicador: Public Library of Science
Tipo: Artigo de Revista Científica
Relevância na Pesquisa
46.15%
As a higher cognitive function in humans, mathematics is supported by parietal and prefrontal brain regions. Here, we give an integrative account of the role of the different brain systems in processing the semantics of mathematical logic from the perspective of macroscopic polysynaptic networks. By comparing algebraic and arithmetic expressions of identical underlying structure, we show how the different subparts of a fronto-parietal network are modulated by the semantic domain, over which the mathematical formulae are interpreted. Within this network, the prefrontal cortex represents a system that hosts three major components, namely, control, arithmetic-logic, and short-term memory. This prefrontal system operates on data fed to it by two other systems: a premotor-parietal top-down system that updates and transforms (external) data into an internal format, and a hippocampal bottom-up system that either detects novel information or serves as an access device to memory for previously acquired knowledge.

## A integração do tutorial interativo TryLogic via IMS Learning Tools Interoperability: construindo uma infraestrutura para o ensino de Lógica através de estratégias de demonstração e refutação; The integration of the interactive tutorial TryLogic via IMS Learning Tools Interoperability: constructing a framework to teaching logic by proofs and refutations

Terrematte, Patrick Cesar Alves
Fonte: Universidade Federal do Rio Grande do Norte; BR; UFRN; Programa de Pós-Graduação em Sistemas e Computação; Ciência da Computação Publicador: Universidade Federal do Rio Grande do Norte; BR; UFRN; Programa de Pós-Graduação em Sistemas e Computação; Ciência da Computação
Tipo: Dissertação Formato: application/pdf
POR
Relevância na Pesquisa
46.07%
Logic courses represent a pedagogical challenge and the recorded number of cases of failures and of discontinuity in them is often high. Amont other difficulties, students face a cognitive overload to understand logical concepts in a relevant way. On that track, computational tools for learning are resources that help both in alleviating the cognitive overload scenarios and in allowing for the practical experimenting with theoretical concepts. The present study proposes an interactive tutorial, namely the TryLogic, aimed at teaching to solve logical conjectures either by proofs or refutations. The tool was developed from the architecture of the tool TryOcaml, through support of the communication of the web interface ProofWeb in accessing the proof assistant Coq. The goals of TryLogic are: (1) presenting a set of lessons for applying heuristic strategies in solving problems set in Propositional Logic; (2) stepwise organizing the exposition of concepts related to Natural Deduction and to Propositional Semantics in sequential steps; (3) providing interactive tasks to the students. The present study also aims at: presenting our implementation of a formal system for refutation; describing the integration of our infrastructure with the Virtual Learning Environment Moodle through the IMS Learning Tools Interoperability specification; presenting the Conjecture Generator that works for the tasks involving proving and refuting; and...

## Verification of mathematical design documents

Liu, Zhiying
Fonte: University of Limerick Publicador: University of Limerick
Tipo: Doctoral thesis; all_ul_research; ul_published_reviewed; ul_theses_dissertations; none
EN_US
Relevância na Pesquisa
45.98%
peer-reviewed; The problem to be studied in this thesis is how to verify a set of mathematical design documents in the sense that if each component is implemented correctly, the whole system should work together harmoniously to satisfy the system requirements. In general, a software modular design is often a procedure of 1) decomposition of a complex system into manageable modules that can be developed seperately, 2) specifying and developing each component individually, and 3) combining the components back into a system. The collection of software components that is aimed at finishing a required task together must cooperate with each other through some communication paths. We consider the interconnection description of such a collection of software components as an integral part of a software design. In this thesis, we present an approach to a) describing a network of components, b) checking whether the network is completely connected and whether it is consistent, i.e., whether the components can work together properly, c) determining the behaviour of the network, i.e., what the components will do if they are combined together as described in the network description, and d) checking whether the behavior of the network conforms to the requirements...

## Um estudo sobre as origens da Lógica Matemáitca

Sousa, Giselle Costa de
Fonte: Universidade Federal do Rio Grande do Norte; BR; UFRN; Programa de Pós-Graduação em Educação; Educação Publicador: Universidade Federal do Rio Grande do Norte; BR; UFRN; Programa de Pós-Graduação em Educação; Educação
Tipo: Tese de Doutorado Formato: application/pdf
POR
Relevância na Pesquisa
46.47%
The present study has as objective to explaining about the origins of the mathematical logic. This has its beginning attributed to the autodidactic English mathematician George Boole (1815-1864), especially because his books The Mathematical Analysis of Logic (1847) and An Investigation of the Laws of Thought (1854) are recognized as the inaugural works of the referred branch. However, surprisingly, in the same time another mathematician called Augutus of Morgan (1806-1871) it also published a book, entitled Formal Logic (1847), in defense of the mathematic logic. Even so, times later on this same century, another work named Elements of Logic (1875) it appeared evidencing the Aristotelian logic with Richard Whately (1787-1863), considered the better Aristotelian logical of that time. This way, our research, permeated by the history of the mathematics, it intends to study the logic produced by these submerged personages in the golden age of the mathematics (19th century) to we compare the valid systems in referred period and we clarify the origins of the mathematical logic. For that we looked for to delineate the panorama historical wrapper of this study. We described, shortly, biographical considerations about these three representatives of the logic of the 19th century formed an alliance with the exhibition of their point of view as for the logic to the light of the works mentioned above. In this sense...

## Entre o racional e o justo : a logica e as sentenças judiciais; Between rationality and justice : logic and judicial decisions

Fabricio Vasconcelos Gomes
Fonte: Biblioteca Digital da Unicamp Publicador: Biblioteca Digital da Unicamp
Tipo: Dissertação de Mestrado Formato: application/pdf
Relevância na Pesquisa
46.11%

## Sobre os fundamentos de programação lógica paraconsistente; On the foundations of paraconsistent logic programming

Tarcísio Genaro Rodrigues
Fonte: Biblioteca Digital da Unicamp Publicador: Biblioteca Digital da Unicamp
Tipo: Dissertação de Mestrado Formato: application/pdf
Relevância na Pesquisa
46.14%
A Programação Lógica nasce da interação entre a Lógica e os fundamentos da Ciência da Computação: teorias de primeira ordem podem ser interpretadas como programas de computador. A Programação Lógica tem sido extensamente utilizada em ramos da Inteligência Artificial tais como Representação do Conhecimento e Raciocínio de Senso Comum. Esta aproximação deu origem a uma extensa pesquisa com a intenção de definir sistemas de Programação Lógica paraconsistentes, isto é, sistemas nos quais seja possível manipular informação contraditória. Porém, todas as abordagens existentes carecem de uma fundamentação lógica claramente definida, como a encontrada na programação lógica clássica. A questão básica é saber quais são as lógicas paraconsistentes subjacentes a estas abordagens. A presente dissertação tem como objetivo estabelecer uma fundamentação lógica e conceitual clara e sólida para o desenvolvimento de sistemas bem fundados de Programação Lógica Paraconsistente. Nesse sentido, este trabalho pode ser considerado como a primeira (e bem sucedida) etapa de um ambicioso programa de pesquisa. Uma das teses principais da presente dissertação é que as Lógicas da Inconsistência Formal (LFI's)...

## Proceedings First Symposium on Games, Automata, Logic, and Formal Verification

Montanari, Angelo; Napoli, Margherita; Parente, Mimmo
Tipo: Artigo de Revista Científica
Relevância na Pesquisa
46.01%
This volume contains the Proceedings of the first Symposium on "Games, Automata, Logic, and Formal Verification (GandALF)", held in Minori (Amalfi coast), Italy, 17-18 June 2010. The symposium has been promoted by a number of Italian computer scientists interested in game theory, mathematical logic, automata theory, and their applications to the specification, design, and verification of complex systems. It covers a large spectrum of research topics, ranging from theoretical aspects to concrete applications. Its aim is to provide a forum where people from different areas, and possibly with a different background, can successfully interact. The high-level international profile of the event is witnessed by the composition of the program committee and by the final program.

## Introduction to mathematical logic - A problem solving course

Miller, Arnold W.
Tipo: Artigo de Revista Científica
Relevância na Pesquisa
56.17%
This is a set of 288 questions written for a Moore-style course in Mathematical Logic. I have used these (or some variation) four times in a beginning graduate course. Topics covered are: propositional logic axioms of ZFC wellorderings and equivalents of AC ordinal and cardinal arithmetic first order logic, and the compactness theorem Lowenheim-Skolem theorems Turing machines, Church's Thesis completeness theorem and first incompleteness theorem undecidable theories second incompleteness theorem

## Formalizing common sense for scalable inconsistency-robust information integration using Direct Logic(TM) reasoning and the Actor Model

Hewitt, Carl
Tipo: Artigo de Revista Científica
Relevância na Pesquisa
46.11%
Because contemporary large software systems are pervasively inconsistent, it is not safe to reason about them using classical logic. The goal of Direct Logic is to be a minimal fix to classical mathematical logic that meets the requirements of large-scale Internet applications (including sense making for natural language) by addressing the following issues: inconsistency robustness, contrapositive inference bug, and direct argumentation. Direct Logic makes the following contributions over previous work: * Direct Inference (no contrapositive bug for inference) * Direct Argumentation (inference directly expressed) * Inconsistency-robust deduction without artifices such as indices (labels) on propositions or restrictions on reiteration * Intuitive inferences hold including the following: * Boolean Equivalences * Reasoning by splitting for disjunctive cases * Soundness * Inconsistency-robust Proof by Contradiction Since the global state model of computation (first formalized by Turing) is inadequate to the needs of modern large-scale Internet applications the Actor Model was developed to meet this need. Using, the Actor Model, this paper proves that Logic Programming is not computationally universal in that there are computations that cannot be implemented using logical inference. Consequently the Logic Programming paradigm is strictly less general than the Procedural Embedding of Knowledge paradigm.; Comment: Corrected: all types are strict

## Logic for Everyone

Herrmann, Robert A.
Tipo: Artigo de Revista Científica
Relevância na Pesquisa
46.13%
Presented, in this monograph, are the results of the U. S. Naval Academy Mathematical Logic Course Project. The propositional and predicate calculus is presented in a unique manner. All aspects are rigorously established using the the fewest mathematical techniques. The propositional calculus is expanded considerably and many of the proof methods are used to establish the predicate calculus results. Consequnce operators are also introduced. Further, the material is considered to be a terminal experience and is directed towards applications such as logic-networks, procedures to determine the validity of arguments, the simple consistency of some sets of hypotheses, some concrete and abstract model theory and, by the Compactness Theorem, the generation of infinitesimals, ultrawords and ultralogics.; Comment: 124 pages

## A Tutorial Introduction to the Logic of Parametric Probability

Norman, Joseph W.
Tipo: Artigo de Revista Científica
Relevância na Pesquisa
46.05%
The computational method of parametric probability analysis is introduced. It is demonstrated how to embed logical formulas from the propositional calculus into parametric probability networks, thereby enabling sound reasoning about the probabilities of logical propositions. An alternative direct probability encoding scheme is presented, which allows statements of implication and quantification to be modeled directly as constraints on conditional probabilities. Several example problems are solved, from Johnson-Laird's aces to Smullyan's zombies. Many apparently challenging problems in logic turn out to be simple problems in algebra and computer science: systems of polynomial equations or linear optimization problems. This work extends the mathematical logic and parametric probability methods invented by George Boole.; Comment: 39 pages including 4 page appendix; new title, additional clarifications, correction of bugs introduced into one example in the last revision

## Universal Algebra and Mathematical Logic

Luo, Zhaohua
Tipo: Artigo de Revista Científica
Relevância na Pesquisa
46.01%
In this paper, first-order logic is interpreted in the framework of universal algebra, using the clone theory developed in three previous papers. We first define the free clone T(L, C) of terms of a first order language L over a set C of parameters in a standard way. The free right algebra F(L, C) of formulas over T(L, C) is then generated by atomic formulas. Structures for L over C are represented as perfect valuations of F(L, C), and theories of L are represented as filters of F(L). Finally Godel's completeness theorem and first incompleteness theorem are stated as expected.

## Why teach an introductory course in Mathematical Logic in the Philosophy curriculum?

Oller, Carlos; Couló, Ana
Tipo: Artigo de Revista Científica
Relevância na Pesquisa
56.17%
This paper tries to justify the relevance of an introductory course in Mathematical Logic in the Philosophy curriculum for analyzing philosophical arguments in natural language. It is argued that the representation of the structure of natural language arguments in Freeman's diagramming system can provide an intuitive foundation for the inferential processes involved in the use of First Order Logic natural deduction rules.; Comment: Proceedings of the Fourth International Conference on Tools for Teaching Logic (TTL2015), Rennes, France, June 9-12, 2015. Editors: M. Antonia Huertas, Jo\~ao Marcos, Mar\'ia Manzano, Sophie Pinchinat, Fran\c{c}ois Schwarzentruber

## Introduction to linear logic and ludics, part I

Curien, Pierre-Louis
Tipo: Artigo de Revista Científica
Relevância na Pesquisa
46.07%
This two-parts paper offers a survey of linear logic and ludics, which were introduced by Girard in 1986 and 2001, respectively. Both theories revisit mathematical logic from first principles, with inspiration from and applications to computer science. The present part I covers an introduction to the connectives and proof rules of linear logic, to its decidability properties, and to its models. Part II will deal with proof nets, a graph-like representation of proofs which is one of the major innovations of linear logic, and will present an introduction to ludics.

## The prospects for mathematical logic in the twenty-first century

Buss, Samuel R.; Kechris, Alexander S.; Pillay, Anand; Shore, Richard A.
Tipo: Artigo de Revista Científica
Relevância na Pesquisa
56.17%
The four authors present their speculations about the future developments of mathematical logic in the twenty-first century. The areas of recursion theory, proof theory and logic for computer science, model theory, and set theory are discussed independently.; Comment: Association for Symbolic Logic

## Infinitesimals without Logic

Giordano, Paolo
Tipo: Artigo de Revista Científica
Relevância na Pesquisa
46.13%
We introduce the ring of Fermat reals, an extension of the real field containing nilpotent infinitesimals. The construction takes inspiration from Smooth Infinitesimal Analysis (SIA), but provides a powerful theory of actual infinitesimals without any need of a background in mathematical logic. In particular, on the contrary with respect to SIA, which admits models only in intuitionistic logic, the theory of Fermat reals is consistent with classical logic. We face the problem to decide if the product of powers of nilpotent infinitesimals is zero or not, the identity principle for polynomials, the definition and properties of the total order relation. The construction is highly constructive, and every Fermat real admits a clear and order preserving geometrical representation. Using nilpotent infinitesimals, every smooth functions becomes a polynomial because in Taylor's formulas the rest is now zero. Finally, we present several applications to informal classical calculations used in Physics: now all these calculations become rigorous and, at the same time, formally equal to the informal ones. In particular, an interesting rigorous deduction of the wave equation is given, that clarifies how to formalize the approximations tied with Hook's law using this language of nilpotent infinitesimals.; Comment: The first part of the preprint is taken directly form arXiv:0907.1872 The second part is new and contains a list of examples

## Inconsistency Robustness in Logic Programs

Hewitt, Carl
Tipo: Artigo de Revista Científica
Relevância na Pesquisa
46.34%
Inconsistency robustness is "information system performance in the face of continually pervasive inconsistencies." A fundamental principle of Inconsistency Robustness is to make contradictions explicit so that arguments for and against propositions can be formalized. This paper explores the role of Inconsistency Robustness in the history and theory of Logic Programs. Robert Kowalski put forward a bold thesis: "Looking back on our early discoveries, I value most the discovery that computation could be subsumed by deduction." However, mathematical logic cannot always infer computational steps because computational systems make use of arbitration for determining which message is processed next by a recipient that is sent multiple messages concurrently. Since reception orders are in general indeterminate, they cannot be inferred from prior information by mathematical logic alone. Therefore mathematical logic cannot in general implement computation. Over the course of history, the term "Functional Program" has grown more precise and technical as the field has matured. "Logic Program" should be on a similar trajectory. Accordingly, "Logic Program" should have a general precise characterization. In the fall of 1972, different characterizations of Logic Programs that have continued to this day: * A Logic Program uses Horn-Clause syntax for forward and backward chaining * Each computational step (according to Actor Model) of a Logic Program is deductively inferred (e.g. in Direct Logic). The above examples are illustrative of how issues of inconsistency robustness have repeatedly arisen in Logic Programs.; Comment: Limits of Classical Logic

## On Fragments without Implications of both the Full Lambek Logic and some of its Substructural Extensions

García-Cerdaña, Àngel; Verdú, Ventura
Tipo: Artigo de Revista Científica
In this paper we study some fragments without implications of the (Hilbert) full Lambek logic $\mathbf{HFL}$ and also some fragments without implications of some of the substructural extensions of that logic. To do this, we perform an algebraic analysis of the Gentzen systems defined by the substructural calculi $\FL_\sigma$. Such systems are extensions of the full Lambek calculus $\FL$ with the rules codified by a subsequence, $\sigma$, of the sequence $e w_l w_r c$; where $e$ stands for \emph{exchange}, $w_l$ for \emph{left weakening}, $w_r$ for \emph{right weakening}, and $c$ for \emph{contraction}. We prove that these Gentzen systems (in languages without implications) are algebraizable by obtaining their equivalent algebraic semantics. All these classes of algebras are varieties of pointed semilatticed monoids and they can be embedded in their ideal completions. As a consequence of these results, we reveal that the fragments of the Gentzen systems associated with the calculi $\FL_\sigma$ are the restrictions of them to the sublanguages considered, and we also reveal that in these languages, the fragments of the external systems associated with $\FL[\sigma]$ are the external systems associated with the restricted Gentzen systems (i.e....