196:(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.
89:, 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
199:(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.
70:’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
146:, Hiroakira Ono, Makoto Kanzawa, Daniel Leivant, Lev Beklemishev) of Annals of Pure and Applied Logic, Theoretical Computer Science, Information and Computation, Journal of Computer System and Sciences, Fundamenta Informaticae, several volumes of Electronic Notes in Theoretical Computer Science;
234:
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,
78:'s dialogue/game-semantics. This led to a type theory called "Meaning as Use Type Theory". 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
17:
193:(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.
205:(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.
31:) 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. He is the founder of the
179:(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,
131:, coordinator and co-founder (with D. Gabbay), Interest Group in Pure and Applied Logics (IGPL), the clearing house of the European Association for Logic, Language and Information (FoLLI), 1990–present;
190:
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.
217:
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.
32:
326:
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,
330:, 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.
384:
379:
202:
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.)
208:(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.
93:'s notion of direct computation, and a novel approach to the dichotomy "intensional versus extensional" accounts of propositional equality via the
117:
Member of the
Advisory Group to the Rolf Schock Prize in Logic and Philosophy (2008 and 2011) Prize Committee (Royal Swedish Academy of Sciences);
173:(with de Oliveira, A.) The Functional Interpretation of Direct Computations. Electronic Notes in Theoretical Computer Science 269:19-40, 2011.
292:
222:
389:
211:(with Maibaum, T.) Proof Theory and Computer Programming, in Zeitschrift fĂĽr mathematische Logik und Grundlagen der Mathematik 36:389-414.
38:
Ruy de
Queiroz received his B.Eng in Electrical Engineering from Escola Politecnica de Pernambuco in 1980, his M.Sc in Informatics from
39:
235:
Foundations of
Cryptography. He has had seven Ph.D. students in the fields of Mathematical Logic and Theoretical Computer Science.
184:
134:
Guest editor of several volumes (in partnership with several world standing logicians and computer scientists such as John
Baldwin,
94:
394:
282:
63:
82:, where Wittgenstein refers to the universal quantifier only having meaning when one sees what follows from it.
176:
On reduction rules, meaning-as-use, and proof-theoretic semantics, Studia Logica 90(2):211-247, November 2008.
399:
340:
de
Queiroz; de Oliveira (2011). "Propositional equality, identity types, and direct computational paths".
101:
214:
A Proof-Theoretic Account of Programming and the RĂ´le of Reduction Rules, in Dialectica 42(4):265-282.
404:
260:
245:
67:
341:
143:
288:
218:
180:
135:
249:
79:
47:
43:
259:
Overseas Research Student scholarship award, Committee of Vice-Chancellors and Principals,
52:
Proof Theory and Computer Programming. An Essay into the Logical Foundations of Computation
90:
75:
139:
105:
373:
253:
71:
35:(WoLLIC), which has been organised annually since 1994, typically in June or July.
104:, a geometric perspective of natural deduction based on a graph-based account of
16:
86:
364:
100:
Since the early 2000s, Ruy de Queiroz has been investigating, jointly with
85:
Since later in the 1990s, Ruy de Queiroz has been engaged, jointly with
28:
328:
Reports of the Thirteenth International Wittgenstein Symposium 1988
163:
Elected member, Council, Association for Symbolic Logic, 2006-2008.
346:
248:, awarded by The Tinker Foundation, after the nomination given by
15:
150:
62:
In the late 1980s, Ruy de Queiroz has offered a reformulation of
149:
Creator and prime organizer of the series of workshops WoLLIC (
138:, Bruno Poizat, Dexter Kozen, Angus Macintyre, Grigori Mints,
122:
Logic Journal of the Interest Group in Pure and Applied Logics
313:
de Queiroz, R. "Meaning as grammar plus consequences", in
160:, D. Gabbay & J. Woods (eds.), College Publications;
33:
Workshop on Logic, Language, Information and Computation
50:in 1990, for which he defended the Dissertation
8:
42:in 1984, and his Ph.D in Computing from the
365:Ruy Guerra's professional profile home page
281:GABBAY, Dov M.; WOODS, John (2009-04-27).
345:
284:The International Directory of Logicians
124:, Oxford University Press, 1993–present;
273:
129:Journal of Computer System and Sciences
385:21st-century Brazilian mathematicians
380:20th-century Brazilian mathematicians
156:Member of the editorial board of the
7:
158:International Directory of Logicians
40:Universidade Federal de Pernambuco
14:
244:Tinker Visiting Professorship at
108:'s symmetric natural deduction.
151:http://www.cin.ufpe.br/~wollic
1:
66:based on a novel reading of
390:Philosophers of mathematics
95:Curry–Howard correspondence
27:(born January 11, 1958, in
25:Ruy J. Guerra B. de Queiroz
421:
112:Service to the profession
287:. College Publications.
395:Mathematical logicians
64:Martin-Löf type theory
21:
19:
261:University of London
102:Anjolina de Oliveira
246:Stanford University
127:Associate editor,
22:
294:978-1-904987-90-1
239:Honors and awards
223:978-981-4360-95-1
136:Sergei N. Artemov
120:Editor-in-chief,
412:
352:
351:
349:
337:
331:
324:
318:
311:
305:
304:
302:
301:
278:
250:Solomon Feferman
187:, pp. 3–88.
168:Key publications
80:Bertrand Russell
58:Research profile
44:Imperial College
420:
419:
415:
414:
413:
411:
410:
409:
370:
369:
361:
356:
355:
339:
338:
334:
325:
321:
312:
308:
299:
297:
295:
280:
279:
275:
270:
241:
232:
170:
114:
91:Richard Statman
76:Jaakko Hintikka
60:
12:
11:
5:
418:
416:
408:
407:
402:
397:
392:
387:
382:
372:
371:
368:
367:
360:
359:External links
357:
354:
353:
332:
319:
306:
293:
272:
271:
269:
266:
265:
264:
257:
240:
237:
231:
228:
227:
226:
215:
212:
209:
206:
203:
200:
197:
194:
191:
188:
177:
174:
169:
166:
165:
164:
161:
154:
147:
140:Wilfrid Hodges
132:
125:
118:
113:
110:
59:
56:
20:Ruy de Queiroz
13:
10:
9:
6:
4:
3:
2:
417:
406:
403:
401:
400:Living people
398:
396:
393:
391:
388:
386:
383:
381:
378:
377:
375:
366:
363:
362:
358:
348:
343:
336:
333:
329:
323:
320:
316:
310:
307:
296:
290:
286:
285:
277:
274:
267:
262:
258:
255:
254:Grigori Mints
251:
247:
243:
242:
238:
236:
229:
224:
220:
216:
213:
210:
207:
204:
201:
198:
195:
192:
189:
186:
185:1-4020-1270-5
182:
178:
175:
172:
171:
167:
162:
159:
155:
152:
148:
145:
141:
137:
133:
130:
126:
123:
119:
116:
115:
111:
109:
107:
103:
98:
96:
92:
88:
83:
81:
77:
73:
72:Paul Lorenzen
69:
65:
57:
55:
53:
49:
45:
41:
36:
34:
30:
26:
18:
335:
327:
322:
317:45(1):83-86.
314:
309:
298:. Retrieved
283:
276:
263:, 1985-1987.
233:
157:
128:
121:
99:
84:
68:Wittgenstein
61:
51:
37:
24:
23:
405:1958 births
374:Categories
315:Dialectica
300:2011-07-28
268:References
144:Anuj Dawar
87:Dov Gabbay
347:1107.1901
230:Teaching
256:, 2005;
74:'s and
291:
221:
183:
106:Kneale
48:London
29:Recife
342:arXiv
289:ISBN
252:and
219:ISBN
181:ISBN
376::
153:);
142:,
97:.
54:.
46:,
350:.
344::
303:.
225:.
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.
