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

- FCT - UNL
- Public Library of Science
- 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
- University of Limerick
- Universidade Federal do Rio Grande do Norte; BR; UFRN; Programa de Pós-Graduação em Educação; Educação
- Biblioteca Digital da Unicamp
- Universidade Cornell
- Association for Symbolic Logic
- Mais Publicadores...

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

Fonte: FCT - UNL
Publicador: FCT - UNL

Tipo: Dissertação de Mestrado

Publicado em //2009
ENG

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

Link permanente para citações:

## Mathematical Logic in the Human Brain: Semantics

Fonte: Public Library of Science
Publicador: Public Library of Science

Tipo: Artigo de Revista Científica

Publicado em 03/01/2013
EN

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.

Link permanente para citações:

## 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

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%

#Lógica matemática. Assistente de demonstração. Tutorial interativo. Ensino de lógica#Mathematical logic. Proof assistant. Interactive tutorial. Teaching logic#CNPQ::OUTROS

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

Link permanente para citações:

## Verification of mathematical design documents

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

Link permanente para citações:

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

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%

#Lógica Matemática#Boole, George (1815-1864)#De Morgan, Augustus (1806-1971)#Whately, Richard (1787-1863)#Educação Matemática#Mathematical Logic#Mathematical Education#CNPQ::CIENCIAS HUMANAS::EDUCACAO

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

Link permanente para citações:

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

Fonte: Biblioteca Digital da Unicamp
Publicador: Biblioteca Digital da Unicamp

Tipo: Dissertação de Mestrado
Formato: application/pdf

Publicado em 18/06/2008
PT

Relevância na Pesquisa

46.11%

Muito se fala na qualidade que possuiriam certas sentenças judiciais de serem "lógicas" em algum sentido. O presente trabalho tem por objetivo esclarecer e propor um possível sentido para esta qualidade quando referente a sentenças judiciais, e, secundariamente, analisar se, segundo o sentido adotado, poderiam realmente algumas sentenças judiciais serem lógicas, ou mesmo se todas o seriam. Para tanto, o trabalho parte da análise e adoção de uma particular proposta de demarcação da Lógica, qual seja, aquela que se dá pelo critério da formalidade. A adoção desta proposta traz consigo, além de uma grande quantidade de ferramentas analíticas fornecidas pela Lógica como assim concebida, o condão de mostrar que qualquer consideração sobre a relação entre Lógica e Direito _e profundamente determinada pela maneira como se concebe e se demarca o objeto do estudo lógico, constatação esta que tem sua importância enlevada quando tomamos em conta o fato de que um posicionamento consciente e claro ante tal demarcação frequentemente é omitido nos estudos de lógica jurídica no Brasil; Much is said about a character that certain judicial decisions supposedly have, that of being "logical", in some sense. This work have as a goal to make clear and to propose a suitable meaning for this characther when it refers to judicial decisions...

Link permanente para citações:

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

Fonte: Biblioteca Digital da Unicamp
Publicador: Biblioteca Digital da Unicamp

Tipo: Dissertação de Mestrado
Formato: application/pdf

Publicado em 29/09/2010
PT

Relevância na Pesquisa

46.14%

#Lógica matemática não-clássica#Lógica simbólica e matemática#Inconsistencia (Logica)#Programação lógica#Linguagens formais - Semantica#Non-classical mathematical logic#Symbolic logic and mathematics#Inconsistency (Logic)#Logic programming#Formal languages

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

Link permanente para citações:

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

Fonte: Universidade Cornell
Publicador: Universidade Cornell

Tipo: Artigo de Revista Científica

Publicado em 09/06/2010

Relevância na Pesquisa

46.01%

#Computer Science - Computer Science and Game Theory#Computer Science - Formal Languages and Automata Theory#Computer Science - Logic in Computer Science#F.1.1#F.4.1#F.3.1#F.4.3

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.

Link permanente para citações:

## Introduction to mathematical logic - A problem solving course

Fonte: Universidade Cornell
Publicador: Universidade Cornell

Tipo: Artigo de Revista Científica

Publicado em 15/01/1996

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

Link permanente para citações:

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

Fonte: Universidade Cornell
Publicador: Universidade Cornell

Tipo: Artigo de Revista Científica

Relevância na Pesquisa

46.11%

#Computer Science - Logic in Computer Science#Computer Science - Programming Languages#Computer Science - Software Engineering

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

Link permanente para citações:

## Logic for Everyone

Fonte: Universidade Cornell
Publicador: Universidade Cornell

Tipo: Artigo de Revista Científica

Publicado em 29/01/2006

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

Link permanente para citações:

## A Tutorial Introduction to the Logic of Parametric Probability

Fonte: Universidade Cornell
Publicador: Universidade Cornell

Tipo: Artigo de Revista Científica

Relevância na Pesquisa

46.05%

#Mathematics - Logic#Computer Science - Logic in Computer Science#Mathematics - Optimization and Control#Mathematics - Probability#03A05, 68N17, 03B42, 97K50, 90C05, 90C26

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

Link permanente para citações:

## Universal Algebra and Mathematical Logic

Fonte: Universidade Cornell
Publicador: Universidade Cornell

Tipo: Artigo de Revista Científica

Publicado em 24/04/2011

Relevância na Pesquisa

46.01%

#Mathematics - Logic#Computer Science - Formal Languages and Automata Theory#Computer Science - Logic in Computer Science

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.

Link permanente para citações:

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

Fonte: Universidade Cornell
Publicador: Universidade Cornell

Tipo: Artigo de Revista Científica

Publicado em 13/07/2015

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

Link permanente para citações:

## Introduction to linear logic and ludics, part I

Fonte: Universidade Cornell
Publicador: Universidade Cornell

Tipo: Artigo de Revista Científica

Publicado em 18/01/2005

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.

Link permanente para citações:

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

Fonte: Universidade Cornell
Publicador: Universidade Cornell

Tipo: Artigo de Revista Científica

Publicado em 03/05/2002

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

Link permanente para citações:

## Infinitesimals without Logic

Fonte: Universidade Cornell
Publicador: Universidade Cornell

Tipo: Artigo de Revista Científica

Publicado em 22/09/2009

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

Link permanente para citações:

## Inconsistency Robustness in Logic Programs

Fonte: Universidade Cornell
Publicador: Universidade Cornell

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

Link permanente para citações:

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

Fonte: Universidade Cornell
Publicador: Universidade Cornell

Tipo: Artigo de Revista Científica

Publicado em 08/07/2013

Relevância na Pesquisa

46.11%

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

Link permanente para citações:

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

Fonte: Association for Symbolic Logic
Publicador: Association for Symbolic Logic

Tipo: Article; PeerReviewed
Formato: application/pdf

Publicado em /06/2001

Relevância na Pesquisa

56.13%

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.

Link permanente para citações: