Ruy de Queiroz

Last updated
Ruy de Queiroz Ruy de Queiroz bw.jpg
Ruy de Queiroz

Ruy J. Guerra B. de Queiroz (born January 11, 1958, in Recife) is an associate professor at Universidade Federal de Pernambuco and holds significant works in the research fields of Mathematical logic, proof theory, foundations of mathematics and philosophy of mathematics. [1] He is the founder of the Workshop on Logic, Language, Information and Computation (WoLLIC), which has been organised annually since 1994, typically in June or July.

Contents

Ruy de Queiroz received his B.Eng in Electrical Engineering from Escola Politecnica de Pernambuco in 1980, his M.Sc in Informatics from Universidade Federal de Pernambuco in 1984, and his Ph.D in Computing from the Imperial College, London in 1990, for which he defended the Dissertation Proof Theory and Computer Programming. An Essay into the Logical Foundations of Computation.

Research profile

In the late 1980s, Ruy de Queiroz has offered a reformulation of Martin-Löf type theory based on a novel reading of Wittgenstein’s "meaning-is-use", where the explanation of the consequences of a given proposition gives the meaning to the logical constant dominating the proposition. This amounts to a non-dialogical interpretation of logical constants via the effect of elimination rules over introduction rules, which finds a parallel in Paul Lorenzen's and Jaakko Hintikka's dialogue/game-semantics. This led to a type theory called "Meaning as Use Type Theory". [2] In reference to the use of Wittgenstein's dictum, he has shown that the aspect concerning the explanation of the consequences of a proposition is present since a very early date when in a letter to Bertrand Russell, where Wittgenstein refers to the universal quantifier only having meaning when one sees what follows from it. [3]

Since later in the 1990s, Ruy de Queiroz has been engaged, jointly with Dov Gabbay, in a program of providing a general account of the functional interpretation of classical and non-classical logics via the notion of labeled natural deduction. As a result, novel accounts of the functional interpretation of the existential quantifier, as well as the notion of propositional equality, were put forward, the latter allowing for a recasting of Richard Statman's notion of direct computation, and a novel approach to the dichotomy "intensional versus extensional" accounts of propositional equality via the Curry–Howard correspondence.

Since the early 2000s, Ruy de Queiroz has been investigating, jointly with Anjolina de Oliveira, a geometric perspective of natural deduction based on a graph-based account of Kneale's symmetric natural deduction. [4]

Service to the profession

Key publications

  1. (with de Oliveira, A.) The Functional Interpretation of Direct Computations. Electronic Notes in Theoretical Computer Science 269:19-40, 2011.
  2. On reduction rules, meaning-as-use, and proof-theoretic semantics, Studia Logica 90(2):211-247, November 2008.
  3. (with de Oliveira, A.) Geometry of Deduction via Graphs of Proof. In Logic for Concurrency and Synchronisation, R. de Queiroz (ed.), volume 18 of the Trends in Logic series, Kluwer Acad. Pub., Dordrecht, July 2003, ISBN   1-4020-1270-5, pp. 3–88.
  4. Meaning, function, purpose, usefulness, consequences - interconnected concepts. Logic Journal of the Interest Group in Pure and Applied Logics, 9(5):693-734, September 2001, Oxford Univ. Press.
  5. (with Gabbay, D.) Labelled Natural Deduction. In Logic, Language and Reasoning. Essays in Honor of Dov Gabbay, H.J. Ohlbach and U. Reyle (eds.), volume 5 of Trends in Logic series, Kluwer Academic Publishers, Dordrecht, June 1999, pp. 173–250.
  6. (with de Oliveira, A.) A Normalization Procedure for the Equational Fragment of Labelled Natural Deduction. Logic Journal of the Interest Group in Pure and Applied Logics, 7(2):173-215, 1999, Oxford Univ. Press. Full version of a paper presented at 2nd WoLLIC'95, Recife, Brazil, July 1995. Abstract appeared in Journal of the Interest Group in Pure and Applied Logics 4(2):330-332, 1996.
  7. (with Gabbay, D.) The Functional Interpretation of the Existential Quantifier, in Bulletin of the Interest Group in Pure and Applied Logics 3(2-3):243-290, 1995. (Special Issue on Deduction and Language, Guest Editor: Ruth Kempson). Full version of a paper presented at Logic Colloquium '91, Uppsala. Abstract in JSL 58(2):753-754, 1993.
  8. Normalisation and Language-Games. In Dialectica 48(2):83-123, 1994. (Early version presented at Logic Colloquium '88, Padova. Abstract in JSL 55:425, 1990.)
  9. (with Gabbay, D.) Extending the Curry-Howard interpretation to linear, relevant and other resource logics, in Journal of Symbolic Logic 57(4):1319-1365. Paper presented at Logic Colloquium '90, Helsinki. Abstract in JSL 56(3):1139-1140, 1991.
  10. (with Maibaum, T.) Abstract Data Types and Type Theory: Theories as Types, in Zeitschrift für mathematische Logik und Grundlagen der Mathematik 37:149-166.
  11. (with Maibaum, T.) Proof Theory and Computer Programming, in Zeitschrift für mathematische Logik und Grundlagen der Mathematik 36:389-414.
  12. A Proof-Theoretic Account of Programming and the Rôle of Reduction Rules, in Dialectica 42(4):265-282.
  13. de Queiroz, R. de Oliveira, A., & Gabbay, D.: 2011, The Functional Interpretation of Logical Deduction. Vol. 5 of Advances in Logic series. Imperial College Press / World Scientific. ISBN   978-981-4360-95-1.

Teaching

Ruy de Queiroz has taught several disciplines related to logic and theoretical computer science, including Set Theory, Recursion Theory (as a follow-up to a course given by Solomon Feferman), Logic for Computer Science, Discrete Mathematics, Theory of Computation, Proof Theory, Model Theory, Foundations of Cryptography. He has had seven Ph.D. students in the fields of Mathematical Logic and Theoretical Computer Science.

Honors and awards

Related Research Articles

The propositional calculus is a branch of logic. It is also called propositional logic, statement logic, sentential calculus, sentential logic, or sometimes zeroth-order logic. It deals with propositions and relations between propositions, including the construction of arguments based on them. Compound propositions are formed by connecting propositions by logical connectives representing the truth functions of conjunction, disjunction, implication, biconditional, and negation. Some sources include other connectives, as in the table below.

Mathematical logic is the study of formal logic within mathematics. Major subareas include model theory, proof theory, set theory, and recursion theory. Research in mathematical logic commonly addresses the mathematical properties of formal systems of logic such as their expressive or deductive power. However, it can also include uses of logic to characterize correct mathematical reasoning or to establish foundations of mathematics.

In logic and proof theory, natural deduction is a kind of proof calculus in which logical reasoning is expressed by inference rules closely related to the "natural" way of reasoning. This contrasts with Hilbert-style systems, which instead use axioms as much as possible to express the logical laws of deductive reasoning.

The history of logic deals with the study of the development of the science of valid inference (logic). Formal logics developed in ancient times in India, China, and Greece. Greek methods, particularly Aristotelian logic as found in the Organon, found wide application and acceptance in Western science and mathematics for millennia. The Stoics, especially Chrysippus, began the development of predicate logic.

Proof theory is a major branch of mathematical logic and theoretical computer science within which proofs are treated as formal mathematical objects, facilitating their analysis by mathematical techniques. Proofs are typically presented as inductively-defined data structures such as lists, boxed lists, or trees, which are constructed according to the axioms and rules of inference of a given logical system. Consequently, proof theory is syntactic in nature, in contrast to model theory, which is semantic in nature.

In programming language theory and proof theory, the Curry–Howard correspondence is the direct relationship between computer programs and mathematical proofs.

Metalogic is the metatheory of logic. Whereas logic studies how logical systems can be used to construct valid and sound arguments, metalogic studies the properties of logical systems. Logic concerns the truths that may be derived using a logical system; metalogic concerns the truths that may be derived about the languages and systems that are used to express truths.

In programming language theory, semantics is the rigorous mathematical study of the meaning of programming languages. Semantics assigns computational meaning to valid strings in a programming language syntax. It is closely related to, and often crosses over with, the semantics of mathematical proofs.

Game semantics is an approach to formal semantics that grounds the concepts of truth or validity on game-theoretic concepts, such as the existence of a winning strategy for a player, somewhat resembling Socratic dialogues or medieval theory of Obligationes.

In logic, a logical framework provides a means to define a logic as a signature in a higher-order type theory in such a way that provability of a formula in the original logic reduces to a type inhabitation problem in the framework type theory. This approach has been used successfully for (interactive) automated theorem proving. The first logical framework was Automath; however, the name of the idea comes from the more widely known Edinburgh Logical Framework, LF. Several more recent proof tools like Isabelle are based on this idea. Unlike a direct embedding, the logical framework approach allows many logics to be embedded in the same type system.

In proof theory, ludics is an analysis of the principles governing inference rules of mathematical logic. Key features of ludics include notion of compound connectives, using a technique known as focusing or focalisation, and its use of locations or loci over a base instead of propositions.

<span class="mw-page-title-main">Logic in computer science</span> Academic discipline

Logic in computer science covers the overlap between the field of logic and that of computer science. The topic can essentially be divided into three main areas:

Giorgi Japaridze is a Georgian-American researcher in logic and theoretical computer science. He currently holds the title of Full Professor at the Computing Sciences Department of Villanova University. Japaridze is best known for his invention of computability logic, cirquent calculus, and Japaridze's polymodal logic.

Non-classical logics are formal systems that differ in a significant way from standard logical systems such as propositional and predicate logic. There are several ways in which this is commonly the case, including by way of extensions, deviations, and variations. The aim of these departures is to make it possible to construct different models of logical consequence and logical truth.

WoLLIC, the Workshop on Logic, Language, Information and Computation is an academic conference in the field of pure and applied logic and theoretical computer science. WoLLIC has been organised annually since 1994, typically in June or July; the conference is scientifically sponsored by the Association for Logic, Language and Information, the Association for Symbolic Logic, the European Association for Theoretical Computer Science and the European Association for Computer Science Logic.

Dialogical logic was conceived as a pragmatic approach to the semantics of logic that resorts to concepts of game theory such as "winning a play" and that of "winning strategy".

<span class="mw-page-title-main">Sergei N. Artemov</span> Russian-American researcher

Sergei Nikolaevich Artemov is a Russian-American researcher in logic and its applications. He currently holds the title of Distinguished Professor at the Graduate Center of the City University of New York where he is the founder and head of its research laboratory for logic and computation. His research interests include proof theory and logic in computer science, optimal control and hybrid systems, automated deduction and verification, epistemology, and epistemic game theory. He is best known for his invention of logics of proofs and justifications.

<span class="mw-page-title-main">Valeria de Paiva</span> Brazilian mathematician, logician, and computer scientist

Valeria Correa Vaz de Paiva is a Brazilian mathematician, logician, and computer scientist. Her work includes research on logical approaches to computation, especially using category theory, knowledge representation and natural language semantics, and functional programming with a focus on foundations and type theories.

This is a glossary of logic. Logic is the study of the principles of valid reasoning and argumentation.

References

  1. ↑ GABBAY, Dov M.; WOODS, John (2009-04-27). The International Directory of Logicians. College Publications. ISBN   978-1-904987-90-1 . Retrieved 2011-07-28.
  2. ↑ de Queiroz, R. "Meaning as grammar plus consequences", in Dialectica 45(1):83-86.
  3. ↑ de Queiroz, R. "The mathematical language and its semantics: to show the consequences of a proposition is to give its meaning". In Weingartner, Paul and Schurz, Gerhard, editors, Reports of the Thirteenth International Wittgenstein Symposium 1988, volume 18 of Schriftenreihe der Wittgenstein-Gesellschaft, Vienna, 304pp. Hölder–Pichler–Tempsky, pp. 259–266. Symposium held in Kirchberg/Wechsel, Austria, August 14–21, 1988.
  4. ↑ de Queiroz; de Oliveira (2011). "Propositional equality, identity types, and direct computational paths". arXiv: 1107.1901 [cs.LO].
This page is based on this Wikipedia article
Text is available under the CC BY-SA 4.0 license; additional terms may apply.
Images, videos and audio are available under their respective licenses.