[Logica-l] Noam Chomsky Suffered ‘Massive Stroke,’ Recovering in Brazil | TIME

2024-06-15 Por tôpico Ruy de Queiroz


https://time.com/6987747/noam-chomsky-stroke-brazil/

-- 
LOGICA-L
Lista acadêmica brasileira dos profissionais e estudantes da área de Lógica 

--- 
Você está recebendo esta mensagem porque se inscreveu no grupo "LOGICA-L" dos 
Grupos do Google.
Para cancelar inscrição nesse grupo e parar de receber e-mails dele, envie um 
e-mail para logica-l+unsubscr...@dimap.ufrn.br.
Para acessar esta discussão na web, acesse 
https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/A67434C8-5DB3-49B6-B902-E6C17B7B27D0%40cin.ufpe.br.


[Logica-l] Game Theory Can Make AI More Correct and Efficient | Quanta Magazine

2024-05-12 Por tôpico Ruy de Queiroz


https://www.quantamagazine.org/game-theory-can-make-ai-more-correct-and-efficient-20240509/

-- 
LOGICA-L
Lista acadêmica brasileira dos profissionais e estudantes da área de Lógica 

--- 
Você está recebendo esta mensagem porque se inscreveu no grupo "LOGICA-L" dos 
Grupos do Google.
Para cancelar inscrição nesse grupo e parar de receber e-mails dele, envie um 
e-mail para logica-l+unsubscr...@dimap.ufrn.br.
Para acessar esta discussão na web, acesse 
https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/DBB91F25-02B6-4B3D-BF62-F0777D3564A7%40cin.ufpe.br.


[Logica-l] 2024 Abel prize: Michel Talagrand wins maths award for making sense of randomness | New Scientist

2024-03-23 Por tôpico Ruy de Queiroz
“ Perhaps inspired by his own work, Talagrand says he sees his career as a 
random process. “It’s absolutely frightening if I look at my life and the 
important things which happened, they are determined by minor random 
influences, and there is no planning whatsoever,” he says.”
https://www.newscientist.com/article/2423192-mathematician-wins-2024-abel-prize-for-making-sense-of-randomness/


-- 
LOGICA-L
Lista acadêmica brasileira dos profissionais e estudantes da área de Lógica 

--- 
Você está recebendo esta mensagem porque se inscreveu no grupo "LOGICA-L" dos 
Grupos do Google.
Para cancelar inscrição nesse grupo e parar de receber e-mails dele, envie um 
e-mail para logica-l+unsubscr...@dimap.ufrn.br.
Para acessar esta discussão na web, acesse 
https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/9CEB80B4-63EF-46CF-8E96-9A6C5D12CA23%40cin.ufpe.br.


[Logica-l] Never-Repeating Tiles Can Safeguard Quantum Information | Quanta Magazine

2024-02-25 Por tôpico Ruy de Queiroz


https://www.quantamagazine.org/never-repeating-tiles-can-safeguard-quantum-information-20240223/


-- 
LOGICA-L
Lista acadêmica brasileira dos profissionais e estudantes da área de Lógica 

--- 
Você está recebendo esta mensagem porque se inscreveu no grupo "LOGICA-L" dos 
Grupos do Google.
Para cancelar inscrição nesse grupo e parar de receber e-mails dele, envie um 
e-mail para logica-l+unsubscr...@dimap.ufrn.br.
Para acessar esta discussão na web, acesse 
https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/4541AE15-2E28-4C3F-8D43-617CC3A87BE0%40cin.ufpe.br.


[Logica-l] Quantum annealers and the future of prime factorization

2024-02-21 Por tôpico Ruy de Queiroz
“Beyond factorization
Prof. Sebastiani emphasized the potential to extend the use of these devices 
beyond prime factorization, envisioning applications in encoding and checking 
the satisfiability of various circuits.

"We believe that quantum annealers can be used to encode and check the 
satisfiability of many other circuits of interest. Thus addressing the 
propositional satisfiability of Boolean circuits (SAT)—a far more general 
problem than prime factorization and allows for representing a variety of 
real-world problems," shared Prof. Sebastiani.”

https://techxplore.com/news/2024-02-quantum-annealers-future-prime-factorization.html

-- 
LOGICA-L
Lista acadêmica brasileira dos profissionais e estudantes da área de Lógica 

--- 
Você está recebendo esta mensagem porque se inscreveu no grupo "LOGICA-L" dos 
Grupos do Google.
Para cancelar inscrição nesse grupo e parar de receber e-mails dele, envie um 
e-mail para logica-l+unsubscr...@dimap.ufrn.br.
Para acessar esta discussão na web, acesse 
https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/E3A238EE-D225-4AE5-A9D9-43B4ADEB3040%40cin.ufpe.br.


[Logica-l] Google DeepMind used a large language model to discover new math | MIT Technology Review

2023-12-17 Por tôpico Ruy de Queiroz


https://www.technologyreview.com/2023/12/14/1085318/google-deepmind-large-language-model-solve-unsolvable-math-problem-cap-set/


-- 
LOGICA-L
Lista acadêmica brasileira dos profissionais e estudantes da área de Lógica 

--- 
Você está recebendo esta mensagem porque se inscreveu no grupo "LOGICA-L" dos 
Grupos do Google.
Para cancelar inscrição nesse grupo e parar de receber e-mails dele, envie um 
e-mail para logica-l+unsubscr...@dimap.ufrn.br.
Para acessar esta discussão na web, acesse 
https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/0E278AE8-FFAF-4B24-AAC6-83EA2153CE9D%40cin.ufpe.br.


[Logica-l] The Astonishing Behavior of Recursive Sequences | Quanta Magazine

2023-11-16 Por tôpico Ruy de Queiroz
The Astonishing Behavior of Recursive SequencesBy ALEX STONENovember 16, 2023Some strange mathematical sequences are always whole numbers — until they’re not. The puzzling patterns have revealed ties to graph theory and prime numbers, awing mathematicians.https://www.quantamagazine.org/the-astonishing-behavior-of-recursive-sequences-20231116/



-- 
LOGICA-L
Lista acadêmica brasileira dos profissionais e estudantes da área de Lógica 
--- 
Você recebeu essa mensagem porque está inscrito no grupo "LOGICA-L" dos Grupos do Google.
Para cancelar inscrição nesse grupo e parar de receber e-mails dele, envie um e-mail para logica-l+unsubscr...@dimap.ufrn.br.
Para acessar essa discussão na Web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/103ACBD1-D72C-4E4D-9056-B05D729BE62D%40cin.ufpe.br.


[Logica-l] Recounting the History of Math’s Transcendental Numbers | Quanta Magazine

2023-06-29 Por tôpico Ruy de Queiroz
“Transcendental numbers include famous examples like e and π, but it took 
mathematicians centuries to understand them.”
https://www.quantamagazine.org/recounting-the-history-of-maths-transcendental-numbers-20230627/



-- 
LOGICA-L
Lista acadêmica brasileira dos profissionais e estudantes da área de Lógica 

--- 
Você está recebendo esta mensagem porque se inscreveu no grupo "LOGICA-L" dos 
Grupos do Google.
Para cancelar inscrição nesse grupo e parar de receber e-mails dele, envie um 
e-mail para logica-l+unsubscr...@dimap.ufrn.br.
Para ver esta discussão na web, acesse 
https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/47985790-BB66-48CB-B52E-1219F8A578F5%40cin.ufpe.br.


[Logica-l] Embracing change and resetting expectations | Microsoft Unlocked

2023-06-29 Por tôpico Ruy de Queiroz
“The 2023-level AI can already generate suggestive hints and promising leads to 
a working mathematician and participate actively in the decision-making 
process. When integrated with tools such as formal proof verifiers, internet 
search, and symbolic math packages, I expect, say, 2026-level AI, when used 
properly, will be a trustworthy co-author in mathematical research, and in many 
other fields as well.”
https://unlocked.microsoft.com/ai-anthology/terence-tao/



-- 
LOGICA-L
Lista acadêmica brasileira dos profissionais e estudantes da área de Lógica 

--- 
Você está recebendo esta mensagem porque se inscreveu no grupo "LOGICA-L" dos 
Grupos do Google.
Para cancelar inscrição nesse grupo e parar de receber e-mails dele, envie um 
e-mail para logica-l+unsubscr...@dimap.ufrn.br.
Para ver esta discussão na web, acesse 
https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/D467BCCF-6E4A-49BD-BDAE-F57DAA8C48AC%40cin.ufpe.br.


[Logica-l] Mathematicians Complete Quest to Build ‘Spherical Cubes’ | Quanta Magazine

2023-02-14 Por tôpico Ruy de Queiroz


https://www.quantamagazine.org/mathematicians-complete-quest-to-build-spherical-cubes-20230210/


-- 
LOGICA-L
Lista acadêmica brasileira dos profissionais e estudantes da área de Lógica 

--- 
Você está recebendo esta mensagem porque se inscreveu no grupo "LOGICA-L" dos 
Grupos do Google.
Para cancelar inscrição nesse grupo e parar de receber e-mails dele, envie um 
e-mail para logica-l+unsubscr...@dimap.ufrn.br.
Para ver esta discussão na web, acesse 
https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/A12DB977-739A-4909-9E74-7F64FBC17B52%40cin.ufpe.br.


[Logica-l] ‘Nasty’ Geometry Breaks Decades-Old Tiling Conjecture | Quanta Magazine

2022-12-17 Por tôpico Ruy de Queiroz


https://www.quantamagazine.org/nasty-geometry-breaks-decades-old-tiling-conjecture-20221215/



-- 
LOGICA-L
Lista acadêmica brasileira dos profissionais e estudantes da área de Lógica 

--- 
Você está recebendo esta mensagem porque se inscreveu no grupo "LOGICA-L" dos 
Grupos do Google.
Para cancelar inscrição nesse grupo e parar de receber e-mails dele, envie um 
e-mail para logica-l+unsubscr...@dimap.ufrn.br.
Para ver esta discussão na web, acesse 
https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/31C31F1E-54D7-401A-BAB0-E8DD0DE16C60%40cin.ufpe.br.


[Logica-l] Mathematician who solved prime-number riddle claims new breakthrough

2022-11-12 Por tôpico Ruy de Queiroz


https://www.nature.com/articles/d41586-022-03689-2



-- 
LOGICA-L
Lista acadêmica brasileira dos profissionais e estudantes da área de Lógica 

--- 
Você está recebendo esta mensagem porque se inscreveu no grupo "LOGICA-L" dos 
Grupos do Google.
Para cancelar inscrição nesse grupo e parar de receber e-mails dele, envie um 
e-mail para logica-l+unsubscr...@dimap.ufrn.br.
Para ver esta discussão na web, acesse 
https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/9915B882-3929-4DED-A8DA-D192141EC306%40cin.ufpe.br.


[Logica-l] Teenager Solves Stubborn Riddle About Prime Number Look-Alikes | Quanta Magazine

2022-10-21 Por tôpico Ruy de Queiroz


https://www.quantamagazine.org/teenager-solves-stubborn-riddle-about-prime-number-look-alikes-20221013/



-- 
LOGICA-L
Lista acadêmica brasileira dos profissionais e estudantes da área de Lógica 

--- 
Você está recebendo esta mensagem porque se inscreveu no grupo "LOGICA-L" dos 
Grupos do Google.
Para cancelar inscrição nesse grupo e parar de receber e-mails dele, envie um 
e-mail para logica-l+unsubscr...@dimap.ufrn.br.
Para ver esta discussão na web, acesse 
https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/7F81C975-CBBB-4C11-A70F-3E25F2E7458E%40cin.ufpe.br.


[Logica-l] Fwd: CFP SLALM2014

2014-04-11 Por tôpico Ruy de Queiroz

Início da mensagem encaminhada

 De: slalm2...@dc.uba.ar
 Data: 11 de abril de 2014 15:56:55 BRT
 Assunto: CFP SLALM2014
 
 16th Latin American Symposium on Mathematical Logic
 XVI SLALM- Simposio Latinoamericano de Lógica Matemática.
 Buenos Aires- Argentina
 28th July- 1st August 2014
 http://www-2.dc.uba.ar/congresos/slalm2014/
 
 You are cordially invited to submit a paper to the 16th Latin-American
 Symposium on Mathematical Logic that will take place in Buenos Aires,
 Argentina, from July the 28th to August the 1st.
 
 XVI SLALM will include four tutorial courses in Model Theory,
 Computability Theory, Set Theory and Non-classical Logic. About a hundred
 researchers and students from Latin-America and other continents will
 participate in the meeting.
 
 The Symposium has the scientific sponsorship of the Association for
 Symbolic Logic.
 
 Program Committee:
 Joan Bagaria. University of Barcelona, Spain
 Xavier Caicedo. Universidad de los Andes. Bogotá, Colombia.
 Walter Carnielli. Universidad Estadual de Campinas, Campinas, SP, Brasil.
 Roberto Cignoli. Universidad de Buenos Aires. Buenos Aires, Argentina.
 (Chair)
 Carlos Di Prisco. IVIC, Venezuela.
 José Iovino. Universidad de Texas. San Antoni, USA.
 Franco Montagna. Universidad de Siena. Siena, Italia.
 Theodore Slaman. University of California at Berkeley, USA.
 Charles Steinhorn. Vassar College, USA.
 Ruy de Queiroz. Universidad Federal de Pernambuco, Brasil.
 
 Plenary speakers:
 Boris Zilber (University of Oxford, England)
 Stevo Todorcievic (University of Toronto, Canada)
 Lev Beklemishev (Steklov Mathematical Institute, Moscow, Russia)
 Verónica Becher (University of Buenos Aires, Argentina)
 Oswaldo Chateubriand (Pontificia Universidade Católica de Rio de Janeiro,
 Brasil)
 Peter Jipsen (Chapman University, USA)
 
 Tutorials:
 Set Theory: Menachem Magidor (Hebrew University of Jerusalem, Israel)
 Computability Theory: Antonio Montalbán (University of California,
 Berkeley, USA)
 Model Theory: Kobi Peterzil (Haifa University, Israel)
 Non-Classical Logics: Luca Spada (Dipartimento di Matematica - University
 of Salerno and  Institue for Logic, Language, and Information - University
 of Amsterdam).
 
 Sessions and Invited Speakers:
 Set Theory:
 Coordinated by Joan Bagaria and Carlos Uzcátegui (Universidad de Los
 Andes, Venezuela)
 
 Christina Brech (Departamento de Matemática,  Universidade de São Paulo,
 Brazil)
 Carlos Martínez Ranero (Universidad de Concepción, Chile)
 Matteo Viale (Mathematical Department of Torino University, Italy)
 
 
 
 Model Theory:
 Coordinated by Charles Steinhorn and Alexander Berenstein (Universidad de
 Los Andes, Colombia)
 
 Xavier Vidaux (Universidad de Concepción, Chile)
 Alfredo Dolich (Kingsborough Community College, CUNY, USA)
 Isaac Goldbring (University of Illinois at Chicago)
 Itaï Ben Yaacov (Université Claude Bernard - Lyon 1)
 Vinicius Cifú Lopes (Universidade Federal do ABC)
 
 Computability Theory:
 Coordinated by Theodore Slaman and Carlos Areces (Universidad Nacional de
 Córdoba, Argentina)
 
 Delia Kesner (Laboratoire PPS, CNRS - Université Paris Diderot, France)
 Andy Lewis (London School of Economics, UK)
 Yde Venema (ILLC, Universiteit van Amsterdam, Netherlands)
 
 
 Non-Classical Logics:
 Coordinated by Franco Montagna and Manuela Busaniche (Universidad Nacional
 del Litoral, Argentina)
 
 Leonardo Manuel Cabrer (Dipartimento di Statistica, Informatica,
 Applicazioni G. Parenti Università degli studi di Firenze, Italy)
 José Luis Castiglioni (Departamento de Matemáticas, UNLP, Argentina)
 Marcelo Coniglio (Department of Philosophy, Institute of Philosophy and
 Human Sciences, State University of Campinas, Brazil)
 
 Submissions to the Conference:
 Contributed presentations can be submitted in one of the four parallel
 sessions: Model Theory, Computability Theory, Set Theory and Non-classical
 Logic. More information on the submission procedure, can be found at the
 conference web site
 http://www-2.dc.uba.ar/congresos/slalm2014/
 
 Abstracts of contributed talks will be published in The Bulletin of
 Symbolic Logic.
 
 
 Local Organizer Committee:
 Carlos Areces (UNC, Córdoba)
 Manuela Busaniche(IMAL-CONICET, Santa Fe)
 Santiago Figueira(UBA,Buenos Aires)
 Rafael Grimson (UBA, Buenos Aires)
 Javier Legáis (UBA, Buenos Aires)
 Ricardo Rodríguez (UBA, Buenos Aires)
 Pedro Sánchez Terraf (UNC, Córdoba)
 Hernán San Martín (UNLP, La Plata)
 
 
 Contact details
 Manuela Busaniche: mbusani...@santafe-conicet.gov.ar
 Ricardo Rodríguez: rica...@dc.uba.ar
 
 
 
___
Logica-l mailing list
Logica-l@dimap.ufrn.br
http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l


[Logica-l] Fwd: CFP XVI SLALM - SATELLITE COLLOQUIUM OF PHILOSOPHY OF LOGIC

2014-04-11 Por tôpico Ruy de Queiroz

Início da mensagem encaminhada

 De: slalm2...@dc.uba.ar
 Data: 11 de abril de 2014 16:01:31 BRT
 Assunto: CFP XVI SLALM - SATELLITE COLLOQUIUM OF PHILOSOPHY OF LOGIC
 
 XVI SLALM - SATELLITE COLLOQUIUM OF PHILOSOPHY OF LOGIC
 A TRIBUTE FOR THE 50th ANNIVERSARY OF THOMAS MORO SIMPSON’S FORMAS
 LOGICAS, REALIDAD Y SIGNIFICADO , July 29th 2014
 
 ORGANIZERS: Oswaldo Chateaubriand (PUC-Rio) , Javier Legris (IIEP-BAIRES,
 CONICET-UBA) , Alberto Moretti (UBA, SADAF-CONICET), Eduardo Scarano
 (CIECE- UBA).
 
 Fifty years ago the first edition of the book Formas lógicas, realidad y
 significado by Thomas Moro Simpson was published in Buenos Aires by
 Eudeba, the university press of the UBA. It was one of the first books
 written in Spanish dealing with philosophical problems in Symbolic Logic,
 mainly from the point of view of philosophical analysis, and was highly
 influential in the philosophical community of Spanish speaking countries.
 As a tribute we organized this colloquium about philosophy of logic.
 
 CALL FOR PAPERS
 
 We invite contributions, following the general guidelines for XVI SLALM
 for submissions, indicating the section “Satellite Colloquium Simpson”.
 Abstracts should not exceed two pages.
 It is expected that contributions to the colloquium should be about
 Simpon’s ideas or subjects form the philosophy of logic discussed in his
 book, like, v. g., ontological suppositions in logic, the meaning of
 logical constants, the notion of logical form, the idea of a perfect
 language, the notion of proposition, among others.
 Deadline for submissiones: May 10th, 2014.
 
 The colloquium will be closed with a dialogue with Thomas Moro Simpson
 
 The colloquium is coordinated by:
 Centro de Investigación en Epistemología de las Ciencias Económicas
 (CIECE), FCE-UBA.
 
 More information on the submission procedure, can be found at the
 conference web site   
 http://www-2.dc.uba.ar/congresos/slalm2014/
 
 
___
Logica-l mailing list
Logica-l@dimap.ufrn.br
http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l


[Logica-l] Palestra Polynomial functors, infinity-groupoids, and homotopy type theory, 24/04, 10hs

2014-04-04 Por tôpico Ruy de Queiroz
O Grupo de Lógica e Fundamentos da
Matemáticahttp://dgp.cnpq.br/diretorioc/fontes/detalhegrupo.jsp?grupo=0021101GPX6Z9G
(Centro
de Informática / Departamento de Matemática da UFPE) convida para a
palestra do Prof Joachim Kock http://mat.uab.es/~kock/ (Departament de
Matemàtiques, Universitat Autònoma de Barcelona) a ser realizada:

Dia: 24/04/2014 (5a.feira)
Hora: 10h
Local: Anfiteatro do Centro de Informática da UFPE

Todos são bem-vindos!

Ruy


*Polynomial functors, infinity-groupoids, and homotopy type theory*
Joachim Kock

Polynomial functors are functors between slice categories, built from pullbacks
and their adjoints, which are 'dependent sums' and 'dependent products',
hence are intimately related to type theory.  They make sense
in locally cartesian closed (infinity)-categories.  Already in sets there are
many interesting aspects to the theory, and before moving on to
infinity-groupoids,
I would like to dwell a little bit on elementary aspects with digressions
into algebra, combinatorics, and classical inductive data types.  The cool
thing about infinity-groupoids is that they work very much like sets ---
just better!  From the viewpoint of combinatorics, symmetries are taken
care of automatically.  From more abstract viewpoints (originating in
geometry and topology), 'everything becomes representable', through the
existence of a general object classifier.  This feature of
infinity-groupoids corresponds to the univalence axiom in homotopy type
theory.  Depending on time and interest, I can either go deeper into the
theory of polynomial functors, or go in more abstract directions of higher
topos theory.


*Joachim Kock* fez doutorado em matemática na UFPE em 2000, depois fez
postdocs em Stockholm, Nice e Montréal, e hoje é professor titular na
Universitat Autònoma de Barcelona. Tem trabalhado em geometria algébrica,
álgebra quântica, teoria de categorias e teoria de homotopia.
___
Logica-l mailing list
Logica-l@dimap.ufrn.br
http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l


[Logica-l] WoLLIC 2014 - Chamada de Trabalhos (DATA-LIMITE SE APROXIMA)

2014-03-23 Por tôpico Ruy de Queiroz
 Olkhovikov (Urals State University)
Nicole Schweikardt (Goethe-University Frankfurt am Main)
Sebastiaan Terwijn (Radboud University Nijmegen)

STEERING COMMITTEE
Samson Abramksy, Johan van Benthem, Anuj Dawar, Joe Halpern, Wilfrid
Hodges, Daniel Leivant, Leonid Libkin, Angus Macintyre, Grigori Mints, Luke
Ong, Hiroakira Ono, Ruy de Queiroz.

ORGANISING COMMITTEE
Pablo Barceló (Universidad de Chile) (Local chair)
Anjolina G. de Oliveira (U Fed Pernambuco)
Ruy de Queiroz (U Fed Pernambuco) (co-chair)
Juan Reutter (Pontificia Universidad Católica de Chile)
Cristián Riveros (Pontificia Universidad Católica de Chile)

FURTHER INFORMATION
Contact one of the Co-Chairs of the Organising Committee.

WEB PAGE
http://wollic.org/wollic2014/
___
Logica-l mailing list
Logica-l@dimap.ufrn.br
http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l


[Logica-l] Contribuições de alunos do CIn-UFPE à Wikipédia (em português), 2013.2

2014-03-23 Por tôpico Ruy de Queiroz
Seguem os endereços de verbetes da Wikipédia para os quais contribuíram os
alunos do CIn-UFPE em 2013.2:

*Traduções:*

*Lógica*
 https://pt.wikipedia.org/wiki/L%C3%B3gica_matem%C3%A1tica

Lógica categórica https://pt.wikipedia.org/wiki/Realizabilidade
Realizabilidade https://pt.wikipedia.org/wiki/Realizabilidade
Teoremas da incompletude de
Gödelhttps://pt.wikipedia.org/wiki/Teoremas_da_incompletude_de_Gödel
Teorema da indefinibilidade de
Tarskihttps://pt.wikipedia.org/wiki/Teorema_da_indefinibilidade_de_Tarski
Lema da diagonal https://pt.wikipedia.org/wiki/Lema_da_Diagonal
Jogo de 
Ehrenfeucht-Fraïsséhttps://pt.wikipedia.org/wiki/Jogo_de_Ehrenfeucht-Fraïssé
Many-sorted logic https://pt.wikipedia.org/wiki/Many-sorted_logic
Sentença aberta https://pt.wikipedia.org/wiki/Sentença_aberta
Notação infixa https://pt.wikipedia.org/wiki/Notação_infixa
Modus ponens https://pt.wikipedia.org/wiki/Modus_ponens
Lógica autoepistêmica https://pt.wikipedia.org/wiki/Lógica_autoepistêmica
Lógica Default https://pt.wikipedia.org/wiki/Lógica_Default
Lógica probabilísticahttps://pt.wikipedia.org/wiki/Lógica_probabil%C3%ADstica
Contradição https://pt.wikipedia.org/wiki/Contradição
Teoria das descrições https://pt.wikipedia.org/wiki/Teoria_das_Descrições
Giuseppe Peano https://pt.wikipedia.org/wiki/Giuseppe_Peano
Dialetheismo https://pt.wikipedia.org/wiki/Dialetheismo
Absorção (lógica) https://pt.wikipedia.org/wiki/Absorção_%28lógica%29
Dilema construtivo https://pt.wikipedia.org/wiki/Dilema_construtivo
Semântica de modelo
estávelhttps://pt.wikipedia.org/wiki/Semântica_de_modelo_estável
Inferência incerta https://pt.wikipedia.org/wiki/Inferência_Incerta
Lógica intermediária http://pt.wikipedia.org/wiki/Lógica_intermediária
Lógica Temporal https://pt.wikipedia.org/wiki/Lógica_Temporal
Lógica subjetiva https://pt.wikipedia.org/wiki/Lógica_subjetiva
Lógica temporal de açõeshttps://pt.wikipedia.org/wiki/Lógica_temporal_de_ações
Fundamentos da 
matemáticahttps://pt.wikipedia.org/wiki/Fundamentos_da_matemática
Falácia do apostador https://pt.wikipedia.org/wiki/Falácia_do_apostador
Lógica Linear https://pt.wikipedia.org/wiki/Lógica_Linear
Lógica dinâmica https://pt.wikipedia.org/wiki/Lógica_Dinâmica
Teoria completa https://pt.wikipedia.org/wiki/Teoria_Completa
Lógica em ciência da
computaçãohttps://pt.wikipedia.org/wiki/Lógica_em_ciência_da_computação




*Teoria da Computação*
Computabilidade http://pt.wikipedia.org/wiki/Computabilidade



*Inéditos:*

*Internet, Empreendedorismo e o Vale do Silício*
Silicon Fen http://pt.wikipedia.org/wiki/Silicon_Fen
Produto viável 
mínimohttps://pt.wikipedia.org/wiki/Produto_vi%C3%A1vel_m%C3%ADnimo
Nerds 2.0.1: A Brief History of the
Internethttps://pt.wikipedia.org/wiki/Nerds_2.0.1
Associação Nacional de Capital de
Venturahttp://pt.wikipedia.org/wiki/Associa%C3%A7%C3%A3o_Nacional_de_Capital_de_Ventura_(NVCA)
https://pt.wikipedia.org/wiki/Educa%C3%A7%C3%A3o_empreendedora

*Tecnologia e Convivência*
Lei de acesso à
informaçãohttps://pt.wikipedia.org/wiki/Lei_de_acesso_%C3%A0_informa%C3%A7%C3%A3o
Code: Version 2.0 https://pt.wikipedia.org/wiki/Code:_Version_2.0
___
Logica-l mailing list
Logica-l@dimap.ufrn.br
http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l


[Logica-l] E. W. Beth Dissertation Prize: 2014 call for nominations

2014-02-25 Por tôpico Ruy de Queiroz
E. W. Beth Dissertation Prize: 2014 call for nominations


Since 2002, FoLLI (the Association for Logic, Language, and Information,
http://www.folli.info) has awarded the E.W. Beth Dissertation Prize to
outstanding dissertations in the fields of Logic, Language, and
Information. We invite submissions for the best dissertation which resulted
in a Ph.D. degree awarded in 2013. The dissertations will be judged on
technical depth and strength, originality, and impact made in at least two
of three fields of Logic, Language, and Computation. Interdisciplinarity is
an important feature of the theses competing for the E.W. Beth Dissertation
Prize.


Who qualifies.


Nominations of candidates are admitted who were awarded a Ph.D. degree in
the areas of Logic, Language, or Information between January 1st, 2013 and
December 31st, 2013. Theses must be written in English; however, the
Committee accepts submissions of English translations of theses originally
written in other languages, and for which a PhD was awarded in the
preceding two years (i.e. between January 1st, 2011 and December 31st,
2012). There is no restriction on the nationality of the candidate or on
the university where the Ph.D. was granted.


Prize.


The prize consists of:


-a certificate


-a donation of 2500 euros provided by the E.W. Beth Foundation


-an invitation to submit the thesis (or a revised version of it) to the
FoLLI Publications on Logic, Language and Information (Springer). For
further information on this series see the FoLLI site.


How to submit.


Only electronic submissions are accepted. The following documents are
required:


1. The thesis in pdf format (ps/doc/rtf not accepted).


2. A ten-page abstract of the dissertation in pdf format.


3. A letter of nomination from the thesis supervisor. Self-nominations are
not admitted: each nomination must be sponsored by the thesis supervisor.
The letter of nomination should concisely describe the scope and
significance of the dissertation and state when the degree was officially
awarded.


4. Two additional letters of support, including at least one letter from a
referee not affiliated with the academic institution that awarded the Ph.D.
degree.


All documents must be submitted electronically (preferably as a zip file)
to Ian Pratt-Hartmann (ipr...@cs.man.ac.uk). Hard copy submissions are not
allowed. In case of any problems with the email submission or a lack of
notification within three working days, nominators should write to Ian
Pratt-Hartmann.


Important dates:


Deadline for Submissions: May 5th, 2014.

Notification of Decision: July 14th, 2014.


Committee :



Julian Bradfield (Edinburgh)


Wojciech Buszkowski (Poznan)


Michael Kaminski (Haifa)


Marco Kuhlmann (Linkoping)


Larry Moss (Bloomington)


Ian Pratt-Hartmann (chair) (Manchester)


Ruy de Queiroz (Recife)


Giovanni Sambin (Padua)


Rob van der Sandt (Nijmegen)


Rineke Verbrugge (Groningen)
___
Logica-l mailing list
Logica-l@dimap.ufrn.br
http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l


Re: [Logica-l] Mini-Curso de Homotopy Theory and Type Theory no Verão da Matemática-UFPE

2014-02-17 Por tôpico Ruy de Queiroz
Infelizmente, a vinda de Eric Finster ficou inviabilizada.

O curso está, portanto, CANCELADO.

Pedimos desculpas pelos inconvenientes causados.

Ruy




2014-02-16 7:57 GMT-03:00 Ruy de Queiroz r...@cin.ufpe.br:

 Aula de 2a.feira está CANCELADA!

 O palestrante não conseguiu embarcar e perdeu o vôo.

 Até segunda ordem, o restante do calendário permanece como foi divulgado.

 Ruy


 2014-02-11 20:57 GMT-03:00 Ruy de Queiroz r...@cin.ufpe.br:

 Aqui vão os dados do curso de Eric Finster:

 Período: 17 a 21/02
 17/02: 14h-18h, Sala D-222, Centro de Informática (CIn) da UFPE
 18/02: 08h-12h, Sala D-222, Centro de Informática (CIn) da UFPE
 19/02: 14h-18h, Sala D-222, Centro de Informática (CIn) da UFPE
 20/02: 14h-18h, Sala A-014, Centro de Informática (CIn) da UFPE
 21/02: 14h-18h, Sala A-014, Centro de Informática (CIn) da UFPE

 A quem interessar: o livro Homotopy Type Theory pode ser obtido a
 partir do seguinte endereço: http://homotopytypetheory.org/book/

 Ruy




 2014-01-07 19:32 GMT-03:00 Ruy de Queiroz r...@cin.ufpe.br:

 É com satisfação que confirmamos a oferta de um mini-curso em Teoria da
 Homotopia e Teoria dos Tipos, por Eric Finster (Paris), como parte do
 Programa de Verão 2014 da Matemática (UFPE).

 Período: 17 a 21 de Fevereiro de 2014
 Horário: 14-18hs
 Sala: (a confirmar)

 Para maiores informações sobre inscrições no Programa de Verão 2014 da
 Matemática (UFPE), visite http://www.dmat.ufpe.br/Verao2014/index.html

 Ruy
 --

 Short Course on Homotopy Theory and Type Theory
 
 In this course, I will give a short overview of some classical
 constructions from algebraic topology and homotopy theory, including the
 theory of homotopy groups, homology groups, fibrations and cofibration
 sequences, as well as some basic applications of these tools. I will then
 proceed to detail the connection with intensional type theory, and in
 particular, how some of these constructions can be mimicked in modern proof
 assistants.

 Bio
 ===
 Eric Finster received his Ph.D. in mathematics in 2010 from the
 University of Virginia.  His thesis work concerned stable splittings of
 mapping spaces and spaces of sections derived from a technique in homotopy
 theory known as Goodwillie Calculus.  After graduating, he held
 postdoctoral positions at the École Polytechnique Fédéral de Lausanne in
 Switzerland, and the Institute for Advanced study in Princeton, where he
 participated in the Univalent Foundations project.  His work concerns
 connections between logic, computer science, homotopy theory and higher
 category theory.




___
Logica-l mailing list
Logica-l@dimap.ufrn.br
http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l


Re: [Logica-l] Mini-Curso de Homotopy Theory and Type Theory no Verão da Matemática-UFPE

2014-02-16 Por tôpico Ruy de Queiroz
Aula de 2a.feira está CANCELADA!

O palestrante não conseguiu embarcar e perdeu o vôo.

Até segunda ordem, o restante do calendário permanece como foi divulgado.

Ruy


2014-02-11 20:57 GMT-03:00 Ruy de Queiroz r...@cin.ufpe.br:

 Aqui vão os dados do curso de Eric Finster:

 Período: 17 a 21/02
 17/02: 14h-18h, Sala D-222, Centro de Informática (CIn) da UFPE
 18/02: 08h-12h, Sala D-222, Centro de Informática (CIn) da UFPE
 19/02: 14h-18h, Sala D-222, Centro de Informática (CIn) da UFPE
 20/02: 14h-18h, Sala A-014, Centro de Informática (CIn) da UFPE
 21/02: 14h-18h, Sala A-014, Centro de Informática (CIn) da UFPE

 A quem interessar: o livro Homotopy Type Theory pode ser obtido a partir
 do seguinte endereço: http://homotopytypetheory.org/book/

 Ruy




 2014-01-07 19:32 GMT-03:00 Ruy de Queiroz r...@cin.ufpe.br:

 É com satisfação que confirmamos a oferta de um mini-curso em Teoria da
 Homotopia e Teoria dos Tipos, por Eric Finster (Paris), como parte do
 Programa de Verão 2014 da Matemática (UFPE).

 Período: 17 a 21 de Fevereiro de 2014
 Horário: 14-18hs
 Sala: (a confirmar)

 Para maiores informações sobre inscrições no Programa de Verão 2014 da
 Matemática (UFPE), visite http://www.dmat.ufpe.br/Verao2014/index.html

 Ruy
 --

 Short Course on Homotopy Theory and Type Theory
 
 In this course, I will give a short overview of some classical
 constructions from algebraic topology and homotopy theory, including the
 theory of homotopy groups, homology groups, fibrations and cofibration
 sequences, as well as some basic applications of these tools. I will then
 proceed to detail the connection with intensional type theory, and in
 particular, how some of these constructions can be mimicked in modern proof
 assistants.

 Bio
 ===
 Eric Finster received his Ph.D. in mathematics in 2010 from the
 University of Virginia.  His thesis work concerned stable splittings of
 mapping spaces and spaces of sections derived from a technique in homotopy
 theory known as Goodwillie Calculus.  After graduating, he held
 postdoctoral positions at the École Polytechnique Fédéral de Lausanne in
 Switzerland, and the Institute for Advanced study in Princeton, where he
 participated in the Univalent Foundations project.  His work concerns
 connections between logic, computer science, homotopy theory and higher
 category theory.



___
Logica-l mailing list
Logica-l@dimap.ufrn.br
http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l


Re: [Logica-l] Mini-Curso de Homotopy Theory and Type Theory no Verão da Matemática-UFPE

2014-02-11 Por tôpico Ruy de Queiroz
Aqui vão os dados do curso de Eric Finster:

Período: 17 a 21/02
17/02: 14h-18h, Sala D-222, Centro de Informática (CIn) da UFPE
18/02: 08h-12h, Sala D-222, Centro de Informática (CIn) da UFPE
19/02: 14h-18h, Sala D-222, Centro de Informática (CIn) da UFPE
20/02: 14h-18h, Sala A-014, Centro de Informática (CIn) da UFPE
21/02: 14h-18h, Sala A-014, Centro de Informática (CIn) da UFPE

A quem interessar: o livro Homotopy Type Theory pode ser obtido a partir
do seguinte endereço: http://homotopytypetheory.org/book/

Ruy




2014-01-07 19:32 GMT-03:00 Ruy de Queiroz r...@cin.ufpe.br:

 É com satisfação que confirmamos a oferta de um mini-curso em Teoria da
 Homotopia e Teoria dos Tipos, por Eric Finster (Paris), como parte do
 Programa de Verão 2014 da Matemática (UFPE).

 Período: 17 a 21 de Fevereiro de 2014
 Horário: 14-18hs
 Sala: (a confirmar)

 Para maiores informações sobre inscrições no Programa de Verão 2014 da
 Matemática (UFPE), visite http://www.dmat.ufpe.br/Verao2014/index.html

 Ruy
 --

 Short Course on Homotopy Theory and Type Theory
 
 In this course, I will give a short overview of some classical
 constructions from algebraic topology and homotopy theory, including the
 theory of homotopy groups, homology groups, fibrations and cofibration
 sequences, as well as some basic applications of these tools. I will then
 proceed to detail the connection with intensional type theory, and in
 particular, how some of these constructions can be mimicked in modern proof
 assistants.

 Bio
 ===
 Eric Finster received his Ph.D. in mathematics in 2010 from the
 University of Virginia.  His thesis work concerned stable splittings of
 mapping spaces and spaces of sections derived from a technique in homotopy
 theory known as Goodwillie Calculus.  After graduating, he held
 postdoctoral positions at the École Polytechnique Fédéral de Lausanne in
 Switzerland, and the Institute for Advanced study in Princeton, where he
 participated in the Univalent Foundations project.  His work concerns
 connections between logic, computer science, homotopy theory and higher
 category theory.

___
Logica-l mailing list
Logica-l@dimap.ufrn.br
http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l


[Logica-l] Mini-Curso de Homotopy Theory and Type Theory no Verão da Matemática-UFPE

2014-01-07 Por tôpico Ruy de Queiroz
É com satisfação que confirmamos a oferta de um mini-curso em Teoria da
Homotopia e Teoria dos Tipos, por Eric Finster (Paris), como parte do
Programa de Verão 2014 da Matemática (UFPE).

Período: 17 a 21 de Fevereiro de 2014
Horário: 14-18hs
Sala: (a confirmar)

Para maiores informações sobre inscrições no Programa de Verão 2014 da
Matemática (UFPE), visite http://www.dmat.ufpe.br/Verao2014/index.html

Ruy
--

Short Course on Homotopy Theory and Type Theory

In this course, I will give a short overview of some classical
constructions from algebraic topology and homotopy theory, including the
theory of homotopy groups, homology groups, fibrations and cofibration
sequences, as well as some basic applications of these tools. I will then
proceed to detail the connection with intensional type theory, and in
particular, how some of these constructions can be mimicked in modern proof
assistants.

Bio
===
Eric Finster received his Ph.D. in mathematics in 2010 from the University
of Virginia.  His thesis work concerned stable splittings of mapping spaces
and spaces of sections derived from a technique in homotopy theory known as
Goodwillie Calculus.  After graduating, he held postdoctoral positions at
the École Polytechnique Fédéral de Lausanne in Switzerland, and the
Institute for Advanced study in Princeton, where he participated in the
Univalent Foundations project.  His work concerns connections between
logic, computer science, homotopy theory and higher category theory.
___
Logica-l mailing list
Logica-l@dimap.ufrn.br
http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l


[Logica-l] WoLLIC 2014 - 2a. Chamada de Trabalhos

2013-12-16 Por tôpico Ruy de Queiroz
[Favor divulgar. Desculpas por eventuais duplicações.]


 WoLLIC 2014
21st Workshop on Logic, Language, Information and Computation
September 1st to 4th, 2014
Valparaiso, Chile


SCIENTIFIC SPONSORSHIP
Interest Group in Pure and Applied Logics (IGPL)
The Association for Logic, Language and Information (FoLLI)
Association for Symbolic Logic (ASL)
European Association for Theoretical Computer Science (EATCS)
European Association for Computer Science Logic (EACSL)
Sociedade Brasileira de Computação (SBC)
Sociedade Brasileira de Lógica (SBL)

ORGANISATION
Department of Computer Science, Universidad de Chile, Chile
Department of Computer Science, Pontificia Universidad Católica de Chile,
Chile
Centro de Informática, Universidade Federal de Pernambuco, Brazil

HOSTED BY
Department of Informatics, Universidad Técnica Federico Santa María, Chile

CALL FOR PAPERS
WoLLIC is an annual international forum on inter-disciplinary research
involving formal logic, computing and programming theory, and natural
language and reasoning. Each meeting includes invited talks and tutorials
as well as contributed papers. The twentieth WoLLIC will be held at the
Universidad Técnica Federico Santa María, from September 1st to 4th, 2014.
It is sponsored by the Association for Symbolic Logic (ASL), the Interest
Group in Pure and Applied Logics (IGPL), the The Association for Logic,
Language and Information (FoLLI), the European Association for Theoretical
Computer Science (EATCS), the European Association for Computer Science
Logic (EACSL), the Sociedade Brasileira de Computação (SBC), and the
Sociedade Brasileira de Lógica (SBL).

PAPER SUBMISSION
Contributions are invited on all pertinent subjects, with particular
interest in cross-disciplinary topics. Typical but not exclusive areas of
interest are: foundations of computing and programming; novel computation
models and paradigms; broad notions of proof and belief; proof mining, type
theory, effective learnability; formal methods in software and hardware
development; logical approach to natural language and reasoning; logics of
programs, actions and resources; foundational aspects of information
organization, search, flow, sharing, and protection. Proposed contributions
should be in English, and consist of a scholarly exposition accessible to
the non-specialist, including motivation, background, and comparison with
related works. They must not exceed 10 pages (in font 10 or higher), with
up to 5 additional pages for references and technical appendices. The
paper's main results must not be published or submitted for publication in
refereed venues, including journals and other scientific meetings. It is
expected that each accepted paper be presented at the meeting by one of its
authors. Papers must be submitted electronically at the WoLLIC 2014
EasyChair website. (Please go to
http://wollic.org/wollic2014/instructions.html for instructions.) A title
and single-paragraph abstract should be submitted by Mar 24, 2014, and the
full paper by Mar 28, 2014 (firm date). Notifications are expected by May
2, 2014, and final papers for the proceedings will be due by May 15, 2014
(firm date).

PROCEEDINGS
The proceedings of WoLLIC 2014, including both invited and contributed
papers, will be published in advance of the meeting as a volume in
Springer's LNCS series. In addition, abstracts will be published in the
Conference Report section of the Logic Journal of the IGPL, and selected
contributions will be published as a special post-conference WoLLIC 2014
issue of a scientific journal (to be confirmed).

INVITED SPEAKERS
Verónica Becher (U Buenos Aires)
Juha Kontinen (U Helsinki)
Aarne Ranta (U Gothenburg)
Kazushige Terui (U Kyoto)
Luca Viganò (King’s College London)
Thomas Wilke (U Kiel)

STUDENT GRANTS
ASL sponsorship of WoLLIC 2014 will permit ASL student members to apply for
a modest travel grant (deadline: May 1st, 2014). See
http://www.aslonline.org/studenttravelawards.html for details.

IMPORTANT DATES
Mar 24, 2014: Paper title and abstract deadline
Mar 28, 2014: Full paper deadline
May 2, 2014: Author notification
May 15, 2014: Final version deadline (firm)

PROGRAMME COMMITTEE
Natasha Alechina (U Nottingham)
Eric Allender (Rutgers U)
Marcelo Arenas (PUC Chile)
Steve Awodey (CMU)
Julian Bradfield (U Edinburgh)
Xavier Caicedo (U de Los Andes)
Olivier Danvy (Aarhus U)
Ulrich Kohlenbach (Tech U Darmstadt) (CHAIR)
Marcus Kracht  (U Bielefeld)
Michiel van Lambalgen (U Amsterdam)
 Klaus Meer (Tech U Cottbus)
George Metcalfe (Bern U)
Dale Miller (INRIA Saclay / LIX)
Russell Miller (CUNY)
Sara Negri (U Helsinki)
Nicole Schweikardt  (U Frankfurt)
(more to come)

STEERING COMMITTEE
Samson Abramksy, Johan van Benthem, Anuj Dawar, Joe Halpern, Wilfrid
Hodges, Daniel Leivant, Leonid Libkin, Angus Macintyre, Grigori Mints, Luke
Ong, Hiroakira Ono, Ruy de Queiroz.

ORGANISING COMMITTEE
Pablo Barceló (Universidad de Chile) (Local chair)
Anjolina G. de Oliveira (U Fed Pernambuco)
Ruy de Queiroz (U Fed

[Logica-l] WoLLIC 2014 - 1a. Chamada de Trabalhos

2013-10-12 Por tôpico Ruy de Queiroz
[Favor divulgar. Desculpas pelas repetições.]


WoLLIC 2014
21st Workshop on Logic, Language, Information and Computation
September 1st to 4th, 2014
Valparaiso, Chile


SCIENTIFIC SPONSORSHIP
Interest Group in Pure and Applied Logics (IGPL)
The Association for Logic, Language and Information (FoLLI)
Association for Symbolic Logic (ASL)
European Association for Theoretical Computer Science (EATCS)
European Association for Computer Science Logic (EACSL)
Sociedade Brasileira de Computação (SBC)
Sociedade Brasileira de Lógica (SBL)

ORGANISATION
Department of Computer Science, Universidad de Chile, Chile
Department of Computer Science, Pontificia Universidad Católica de Chile,
Chile
Centro de Informática, Universidade Federal de Pernambuco, Brazil

HOSTED BY
Department of Informatics, Universidad Técnica Federico Santa María, Chile


CALL FOR PAPERS
WoLLIC is an annual international forum on inter-disciplinary research
involving formal logic, computing and programming theory, and natural
language and reasoning. Each meeting includes invited talks and tutorials
as well as contributed papers. The twentieth WoLLIC will be held at the
Universidad Técnica Federico Santa María, from September 1st to 4th, 2014.
It is sponsored by the Association for Symbolic Logic (ASL), the Interest
Group in Pure and Applied Logics (IGPL), the The Association for Logic,
Language and Information (FoLLI), the European Association for Theoretical
Computer Science (EATCS), the European Association for Computer Science
Logic (EACSL), the Sociedade Brasileira de Computação (SBC), and the
Sociedade Brasileira de Lógica (SBL).

PAPER SUBMISSION
Contributions are invited on all pertinent subjects, with particular
interest in cross-disciplinary topics. Typical but not exclusive areas of
interest are: foundations of computing and programming; novel computation
models and paradigms; broad notions of proof and belief; proof mining, type
theory, effective learnability; formal methods in software and hardware
development; logical approach to natural language and reasoning; logics of
programs, actions and resources; foundational aspects of information
organization, search, flow, sharing, and protection. Proposed contributions
should be in English, and consist of a scholarly exposition accessible to
the non-specialist, including motivation, background, and comparison with
related works. They must not exceed 10 pages (in font 10 or higher), with
up to 5 additional pages for references and technical appendices. The
paper's main results must not be published or submitted for publication in
refereed venues, including journals and other scientific meetings. It is
expected that each accepted paper be presented at the meeting by one of its
authors. Papers must be submitted electronically at the WoLLIC 2014
EasyChair website. (Please go to
http://wollic.org/wollic2014/instructions.html for instructions.) A title
and single-paragraph abstract should be submitted by Mar 24, 2014, and the
full paper by Mar 28, 2014 (firm date). Notifications are expected by May
2, 2014, and final papers for the proceedings will be due by May 15, 2014
(firm date).

PROCEEDINGS
The proceedings of WoLLIC 2014, including both invited and contributed
papers, will be published in advance of the meeting as a volume in
Springer's LNCS series. In addition, abstracts will be published in the
Conference Report section of the Logic Journal of the IGPL, and selected
contributions will be published as a special post-conference WoLLIC 2014
issue of a scientific journal (to be confirmed).

INVITED SPEAKERS
(TBA)

STUDENT GRANTS
ASL sponsorship of WoLLIC 2014 will permit ASL student members to apply for
a modest travel grant (deadline: May 1st, 2014). See
http://www.aslonline.org/studenttravelawards.html for details.

IMPORTANT DATES
Mar 24, 2014: Paper title and abstract deadline
Mar 28, 2014: Full paper deadline
May 2, 2014: Author notification
May 15, 2014: Final version deadline (firm)

PROGRAMME COMMITTEE
Natasha Alechina (U Nottingham)
Eric Allender (Rutgers U)
Marcelo Arenas (PUC Chile)
Steve Awodey (CMU)
Julian Bradfield (U Edinburgh)
Xavier Caicedo (U de Los Andes)
Olivier Danvy (Aarhus U)
Ulrich Kohlenbach (Tech U Darmstadt) (CHAIR)
Marcus Kracht  (U Bielefeld)
Michiel van Lambalgen (U Amsterdam)
 Klaus Meer (Tech U Cottbus)
George Metcalfe (Bern U)
Dale Miller (INRIA Saclay / LIX)
Russell Miller (CUNY)
Sara Negri (U Helsinki)
Nicole Schweikardt  (U Frankfurt)
(more to come)

STEERING COMMITTEE
Samson Abramksy, Johan van Benthem, Anuj Dawar, Joe Halpern, Wilfrid
Hodges, Daniel Leivant, Leonid Libkin, Angus Macintyre, Grigori Mints, Luke
Ong, Hiroakira Ono, Ruy de Queiroz.

ORGANISING COMMITTEE
Pablo Barceló (Universidad de Chile) (Local chair)
Anjolina G. de Oliveira (U Fed Pernambuco)
Ruy de Queiroz (U Fed Pernambuco) (co-chair)
Juan Reutter (Pontificia Universidad Católica de Chile)
Cristián Riveros (Pontificia Universidad Católica de Chile)

FURTHER INFORMATION
Contact one

[Logica-l] Voevodsky's Univalent Axiom in Homotopy Type Theory

2013-10-07 Por tôpico Ruy de Queiroz
Philosophical Logic (@logicians)
05/10/13 11:47
Voevodsky’s #Univalence
Axiom in #Homotopy
Type Theory S. Awodey, et al. #math #logic #philosophy ams.org/notices/201309…

___
Logica-l mailing list
Logica-l@dimap.ufrn.br
http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l


[Logica-l] Contribuições de alunos do CIn-UFPE à Wikipédia (em português), 2013.1

2013-09-28 Por tôpico Ruy de Queiroz
Seguem os endereços de verbetes da Wikipédia para os quais contribuíram os
alunos do CIn-UFPE em 2013.1:
*
*
*Lógica*
https://pt.wikipedia.org/wiki/L%C3%B3gica_matem%C3%A1tica
http://pt.wikipedia.org/wiki/Isomorfismo
https://pt.wikipedia.org/wiki/Paradoxos_da_Implica%C3%A7%C3%A3o_Material
https://pt.wikipedia.org/wiki/Teorema_do_ideal_primo_booleano
https://pt.wikipedia.org/wiki/Anatoly_Maltsev
https://pt.wikipedia.org/wiki/M%C3%A9todo_Efetivo
https://pt.wikipedia.org/wiki/Teoria_da_argumenta%C3%A7%C3%A3o
https://pt.wikipedia.org/wiki/Atomismo_l%C3%B3gico
https://pt.wikipedia.org/wiki/Teorema_de_compacidade_de_Barwise
https://pt.wikipedia.org/wiki/Morfismo_(teoria_das_categorias)
https://pt.wikipedia.org/wiki/%C3%81lgebra_Booleana_(estrutura)
http://pt.wikipedia.org/wiki/Ernst_Mally
https://pt.wikipedia.org/wiki/Elimina%C3%A7%C3%A3o_do_Bicondicional
https://pt.wikipedia.org/wiki/Elimina%C3%A7%C3%A3o_da_disjun%C3%A7%C3%A3o
https://pt.wikipedia.org/wiki/Jon_Barwise
https://pt.wikipedia.org/wiki/Peter_Geach
https://pt.wikipedia.org/wiki/L%C3%B3gica_filos%C3%B3fica
https://pt.wikipedia.org/wiki/Sem%C3%A2ntica_formal(l%C3%B3gica)
https://pt.wikipedia.org/wiki/Teorema_de_L%C3%B6b
https://pt.wikipedia.org/wiki/Martin_Hugo_L%C3%B6b
https://pt.wikipedia.org/wiki/Operador_Modal
https://pt.wikipedia.org/wiki/Wikip%C3%A9dia:Tradu%C3%A7%C3%A3o/L%C3%B3gica_din%C3%A2mica(l%C3%B3gica_modal)
https://pt.wikipedia.org/wiki/F%C3%B3rmula_at%C3%B4mica
https://pt.wikipedia.org/wiki/Interpreta%C3%A7%C3%A3o_(l%C3%B3gica)
https://pt.wikipedia.org/wiki/Teoria_da_Infer%C3%AAncia_Indutiva_de_Solomonoff
http://pt.wikipedia.org/wiki/Aritm%C3%A9tica_de_Robinson
https://pt.wikipedia.org/wiki/Augustus_De_Morgan
https://pt.wikipedia.org/wiki/Helena_Rasiowa
https://pt.wikipedia.org/wiki/Dov_Gabbayhttps://en.wikipedia.org/wiki/Dov_Gabbay
https://pt.wikipedia.org/wiki/Hartley_Rogers,_Jr.https://en.wikipedia.org/wiki/Hartley_Rogers,_Jr.
https://pt.wikipedia.org/wiki/Prova_autom%C3%A1tica_de_teoremas
https://pt.wikipedia.org/wiki/Paradoxo_da_loteria
https://pt.wikipedia.org/wiki/Vari%C3%A1vel_proposicional_(matem%C3%A1tica)
http://pt.wikipedia.org/w/index.php?http://pt.wikipedia.org/w/index.php?title=Paradoxo_de_Skolemoldid=36982523
title=Paradoxo_de_Skolemoldid=36982523http://pt.wikipedia.org/w/index.php?title=Paradoxo_de_Skolemoldid=36982523
https://pt.wikipedia.org/wiki/Logica_temporal
http://pt.wikipedia.org/wiki/Paradoxo_do_elevador
http://pt.wikipedia.org/wiki/Geometria_de_zariski
https://pt.wikipedia.org/wiki/Calculus_Ratiocinator
https://pt.wikipedia.org/wiki/As_Leis_do_Pensamento
https://pt.wikipedia.org/wiki/Problema_de_Fun%C3%A7%C3%A3o
https://pt.wikipedia.org/wiki/Introdu%C3%A7%C3%A3o_Bicondicional
https://pt.wikipedia.org/wiki/Impredicatividade
https://pt.wikipedia.org/wiki/Teoria_das_Descri%C3%A7%C3%B5es
http://pt.wikipedia.org/wiki/Estrutura_de_Herbrand
http://pt.wikipedia.org/wiki/John_Etchemendy
http://pt.wikipedia.org/wiki/Interpreta%C3%A7%C3%A3o_de_herbrand
https://pt.wikipedia.org/wiki/Lotfi_Asker_Zadeh
https://pt.wikipedia.org/wiki/Mozi
http://en.wikipedia.org/wiki/Kripke_semantics
https://pt.wikipedia.org/wiki/Sem%C3%A2nticas_de_Kripke
https://pt.wikipedia.org/wiki/Teorema_de_Goodstein
https://pt.wikipedia.org/wiki/Objeto_formal


*Teoria da Computação*
https://pt.wikipedia.org/wiki/Quinto_problema_de_Hilbert
http://pt.wikipedia.org/wiki/Formalismo_de_Backus-Naur_Extendido
http://pt.wikipedia.org/wiki/Linguagem_formal
https://pt.wikipedia.org/wiki/Semi_aut%C3%B4mato
https://pt.wikipedia.org/wiki/Simbolo_%28Formal%29
https://pt.wikipedia.org/wiki/Produ%C3%A7%C3%A3o_%28ci%C3%AAncia_da_computa%C3%A7%C3%A3o%29
https://pt.wikipedia.org/wiki/Turing_Switch
https://pt.wikipedia.org/wiki/M%C3%A1quina_de_Turing_alternada
https://pt.wikipedia.org/wiki/O_de_Kleene
https://pt.wikipedia.org/wiki/Grandes_ordinais_cont%C3%A1veis
https://pt.wikipedia.org/wiki/Espa%C3%A7o_compacto
http://pt.wikipedia.org/wiki/Aut%C3%B4matos_finitos_determin%C3%ADsticos
https://pt.wikipedia.org/wiki/Aut%C3%B4mato_Probabil%C3%ADstico
https://pt.wikipedia.org/wiki/Prova_assistida_por_Computador
https://pt.wikipedia.org/wiki/O_Problema_do_Final_Feliz
https://pt.wikipedia.org/wiki/Jogo_da_vida
https://pt.wikipedia.org/wiki/John_Conway
https://pt.wikipedia.org/wiki/Teoria_combinat%C3%B3ria_dos_jogos
https://pt.wikipedia.org/wiki/Teste_de_Turing
https://pt.wikipedia.org/wiki/Computadores_e_Intelig%C3%AAncia
http://pt.wikipedia.org/wiki/Equa%C3%A7%C3%A3o_diofantina
http://pt.wikipedia.org/wiki/Aut%C3%B4mato
https://pt.wikipedia.org/wiki/Hierarquia_aritm%C3%A9tica
https://pt.wikipedia.org/wiki/NC_%28complexidade%29
https://pt.wikipedia.org/wiki/Diofanto
https://pt.wikipedia.org/wiki/Redutibilidade
https://pt.wikipedia.org/wiki/Hierarquia_Analítica
https://pt.wikipedia.org/wiki/Teorema_de_McNaughton
https://pt.wikipedia.org/wiki/D%C3%A9nes_K%C3%B6nig


*Internet, Empreendedorismo e o Vale do Silício*
https://pt.wikipedia.org/wiki/Y_Combinator_(companhia)

[Logica-l] Steve Awodey: Structuralism, Invariance, and Univalence

2013-07-27 Por tôpico Ruy de Queiroz
Steve Awodey: *Structuralism, Invariance, and
Univalencehttp://www.andrew.cmu.edu/user/awodey/preprints/siu.pdf
* (Workshop CSPM, April 26, 2013 in Toulouse)

Recent advances in foundations have led to some developments that are
significant for the philosophy of mathematics, particularly structuralism.
Specifically, the discovery of an interpretation of Martin-Löf's
constructive type theory into abstract homotopy theory suggests a new
approach to the foundations of mathematics, with both intrinsic geometric
content and a computational implementation. Leading homotopy theorist
Vladimir Voevodsky has initiated an ambitious new program of foundations on
this basis, including a new axiom with both geometric and logical
significance: the Univalence Axiom. It captures the familiar aspect of
informal mathematical practice, according to which one can identify
isomorphic objects. While it is incompatible with conventional foundations,
it is a powerful addition to the framework of homotopical type theory.
___
Logica-l mailing list
Logica-l@dimap.ufrn.br
http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l


[Logica-l] Fwd: [FOM] BLC 2013 + Dummett Day + Postgraduate Day (Leeds, September 2013)

2013-07-17 Por tôpico Ruy de Queiroz
-- Forwarded message --
From: Peter Schuster psch...@maths.leeds.ac.uk
Date: 2013/7/17
Subject: [FOM] BLC 2013 + Dummett Day + Postgraduate Day (Leeds, September
2013)
To: f...@cs.nyu.edu



The British Logic Colloquium will take place at the University of Leeds,
September 5-7 2013, preceded by Dummett Day in celebration of the life and
work of Sir Michael Dummett (September 4-5), and by a BLC Postgraduate day
(September 3-4). These events are supported by the London Mathematical
Society, the BLC, and (for the Dummett Day) the European Research Council
project `The Nature of Representation'. There is a reduced registration fee
if paid by 2nd August 2013 (extended deadline for early bird rates).

For details, including the invited speakers and a registration form, see

  
http://www1.maths.leeds.ac.uk/**~blc2013/http://www1.maths.leeds.ac.uk/~blc2013/

--**--**
--
__**_
FOM mailing list
f...@cs.nyu.edu
http://www.cs.nyu.edu/mailman/**listinfo/fomhttp://www.cs.nyu.edu/mailman/listinfo/fom
___
Logica-l mailing list
Logica-l@dimap.ufrn.br
http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l


Re: [Logica-l] Turing e Post

2013-06-11 Por tôpico Ruy de Queiroz
Caro Rodrigo,

Vale a pena prestar atenção ao que diz o artigo

Turing Oracle Machines, Online Computing, and Three Displacements in
Computability 
Theoryhttp://www.people.cs.uchicago.edu/~soare/History/turing.pdf
Robert I. Soare


sobretudo no que concerne a algumas referências à opinião de Gödel (em
1955) sobre as contribuições de Turing:

“When I first published my paper about undecidable propositions the result
could not be pronounced in this generality, because for the notions of
mechanical procedure and of formal system no mathematically satisfactory
definition had been given at that time. ...
The essential point is to define what a procedure is.”
“That this really is the correct definition of mechanical computability was
established beyond any doubt by Turing.”



Johan von Neumann é outro que se rende à originalidade de Turing, sobretudo
no que diz respeito à noção de máquina/autômato universal:

“An automaton is “universal” if any sequence that can be produced by any
automaton whatsoever can also be produced by this automaton.”
“Turing observed that a completely general description of any conceivable
automaton can be  (in the sense of the above definition) given in a finite
number of words.”
 (“The General and Logical Theory of
Automatahttp://www.sns.ias.edu/~tlusty/courses/InfoInBio/Papers/vonNeumann1951.pdf”,
Setembro 1948)



Sobre a noção de máquina universal, Martin Davis diz:

“People had been thinking about calculating machines for a long time, since
Leibniz’s time and even earlier.
Before Turing the general supposition was that in dealing with such
machines the three categories, machine, program, and data, were entirely
separate entities. The machine was a physical object; today we would call
it hardware. The program was the plan for doing a computation, perhaps
embodied in punched cards or connections of cables in a plugboard. Finally,
the data was the numerical input.
Turing’s universal machine showed that the distinctness of these three
categories is an illusion

The Universal 
Computerhttp://www.philosophie.uni-hamburg.de/Lehre/SS12/55-122-28_/tarski.pdf(2000)



Resolver negativamente o Entscheidungsproblem  de Hilbert através de um
modelo razoavelmente intuitivo de máquina/algoritmo não foi pouca coisa,
principalmente para o próprio desenvolvimento da Lógica Matemática.

Abraço,
Ruy



Em 11 de junho de 2013 21:11, Rodrigo Freire freires...@gmail.comescreveu:

 Caros

 Ótimas respostas.

 Alguns comentários e questões:

 1- Walter: Pelo que me lembro, o livro de computabilidade adota o
 enfoque de Post para as máquinas de Turing, segundo o qual uma máquina
 de Turing é um conjunto finito de quadruplas, e não de quintuplas como
 fez o Turing?

 2- O livro do Martin Davis, computability and unsolvability adota o
 enfoque de Post para máquinas de Turing. (página 5).

 3- O Marcelo Finger respondeu muito bem sobre as motivações políticas
 em torno desse fenômeno de homenagens ao Turing.

 4- O Jean Yves já respondeu a Valeria, mas o Martin Davis é de fato
 uma espécie de filho intelectual do Post.

 5- Entendo que a homenagem ao Turing é uma homenagem à Lógica através
 de uma figura que tem apelo fora do meio restrito de lógicos. Mas acho
 que há alguns exageros. Por exemplo, por que a capa do recém criado
 journal Computability é uma imagem do Turing? Em que isso homenageia
 a lógica? Olhando para os conteúdos já publicados nesse journal, vejo
 que são artigos de computabilidade comparáveis aos que aparecem em
 outras revistas de lógica, e nada especialmente ligado ao Turing.

 6- Enfim, me parece que o Post deveria ser considerado o father of
 computer science e não o Turing, como afirma o Barry Cooper.
 Certamente há pessoas na lista muito mais qualificadas que eu para
 fazer esse tipo de julgamento e eu gostaria de ouvir a opinião dos
 membros da lista sobre isso.

 Abraço
 Rodrigo
 ___
 Logica-l mailing list
 Logica-l@dimap.ufrn.br
 http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l

___
Logica-l mailing list
Logica-l@dimap.ufrn.br
http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l


[Logica-l] Fwd: European Master's Program in Computational Logic

2013-04-28 Por tôpico Ruy de Queiroz
-- Forwarded message --
From: Bertram Fronhöfer bertram.fronhoe...@tu-dresden.de
Date: 2013/4/28
Subject: European Master's Program in Computational Logic
To:




Dear all,

Please spread this information as wide as possible among friends and
colleagues, at your old universities and the places, where you
currently live and work.

Many thanks -- Steffen


*
The European Master's Program in Computational Logic

We are glad to announce to you the possibility to join our European
Master's Program of Computational Logic. This program is offered
jointly at the Free-University of Bozen-Bolzano in Italy, the
Technische Universität Dresden in Germany, the Universidade Nova de
Lisboa in Portugal and the Technische Universität Wien in
Austria. Within this program you have the choice to study at two
/three of the four European universities. In addition you can do your
project work at the National ICT of Australia (NICTA). You will
graduate with a MSc in Computer Science and obtain a multiple
degree. Information on the universities and the program is provided
here:

http://www.emcl-study.eu/home.**html http://www.emcl-study.eu/home.html

Language of instruction is English. Tuition fees are 3.000 EUR (for
non-European students) and 1.000 (for European students) per year. The
ERASMUS-MUNDUS consortium offers tuition fee waivers and small grants
(http://www.emcl-study.eu/**grants.htmlhttp://www.emcl-study.eu/grants.html
).

More information on the application procedure is available from:

http://www.emcl-study.eu/**application.htmlhttp://www.emcl-study.eu/application.html

Application deadline is 31 May, applicants must use our online
application system.

Do not hesitate to contact us again if you have any further questions.

Kind regards -- Steffen Hölldobler

Prof. Dr. Steffen Hoelldobler
International Center for Computational Logic
Technische Universität Dresden
01062 Dresden, Germany

phone: [+49](351)46 33 83 40
fax: [+49](351)46 33 83 42
email: s...@iccl.tu-dresden.de
___
Logica-l mailing list
Logica-l@dimap.ufrn.br
http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l


[Logica-l] Contribuições de alunos do CIn-UFPE à Wikipédia (em português), 2012.2

2013-04-27 Por tôpico Ruy de Queiroz
Seguem os endereços de verbetes da Wikipédia para os quais contribuíram os
alunos do CIn-UFPE em 2012.2:
*
*
*Lógica*
http://pt.wikipedia.org/wiki/Verdade_l%C3%B3gica
http://pt.wikipedia.org/wiki/Begriffsschrift
http://pt.wikipedia.org/wiki/Modelo_de_aritm%C3%A9tica_n%C3%A3o-padr%C3%A3o
http://pt.wikipedia.org/wiki/Equival%C3%AAncia_elementar
http://pt.wikipedia.org/wiki/Segundo_problema_de_Hilbert
http://pt.wikipedia.org/wiki/Corretude_%28l%C3%B3gica%29
http://pt.wikipedia.org/wiki/Defini%C3%A7%C3%A3o
http://pt.wikipedia.org/wiki/L%C3%B3gica_subestrutural
http://pt.wikipedia.org/wiki/Igualdade_l%C3%B3gica
http://pt.wikipedia.org/wiki/Satisfatibilidade_de_Horn
http://pt.wikipedia.org/wiki/Contraposi%C3%A7%C3%A3o
http://pt.wikipedia.org/wiki/Teorema_da_elimina%C3%A7%C3%A3o_do_corte
http://pt.wikipedia.org/wiki/Sequente
http://pt.wikipedia.org/wiki/Tarski%27s_World
http://pt.wikipedia.org/wiki/Paradoxo_de_Quine
http://pt.wikipedia.org/wiki/F%C3%B3rmula_bem_formada
http://pt.wikipedia.org/wiki/Propriedades_de_Normaliza%C3%A7%C3%A3o_(reescrita_abstrata)http://pt.wikipedia.org/wiki/Propriedades_de_Normaliza%C3%A7%C3%A3o_%28reescrita_abstrata%29
http://pt.wikipedia.org/wiki/C%C3%A1lculo_de_sequentes
http://pt.wikipedia.org/wiki/Sistema_axiom%C3%A1tico
http://pt.wikipedia.org/wiki/Axiomas_de_Hilbert
http://pt.wikipedia.org/wiki/L%C3%B3gica_de_ordem_superior
http://pt.wikipedia.org/wiki/Aritm%C3%A9tica_primitiva_recursiva
http://pt.wikipedia.org/wiki/L%C3%B3gica_do_Di%C3%A1logo
http://pt.wikipedia.org/wiki/Minimiza%C3%A7%C3%A3o_de_Circuitos
http://pt.wikipedia.org/wiki/Algoritmo_de_Quine-McCluskey
http://pt.wikipedia.org/wiki/Equissatisfatibilidade
http://pt.wikipedia.org/wiki/Equiconsistência
http://pt.wikipedia.org/wiki/Sistema_de_Hilbert
http://pt.wikipedia.org/wiki/Predicado_(l%C3%B3gica)http://pt.wikipedia.org/wiki/Predicado_%28l%C3%B3gica%29
http://pt.wikipedia.org/wiki/Senten%C3%A7a_(l%C3%B3gica_matem%C3%A1tica)http://pt.wikipedia.org/wiki/Senten%C3%A7a_%28l%C3%B3gica_matem%C3%A1tica%29
http://pt.wikipedia.org/wiki/Valora%C3%A7%C3%A3o_(l%C3%B3gica)http://pt.wikipedia.org/wiki/Valora%C3%A7%C3%A3o_%28l%C3%B3gica%29
http://pt.wikipedia.org/wiki/Teoria_dos_tipos_intuicionista
http://pt.wikipedia.org/wiki/An%C3%A1lise_construtiva
https://pt.wikipedia.org/wiki/Isomorfismo_de_Curry-Howard


*Teoria da Computação*
http://pt.wikipedia.org/wiki/Problema_de_otimiza%C3%A7%C3%A3o
http://pt.wikipedia.org/wiki/Comutatividade_da_conjun%C3%A7%C3%A3o
http://pt.wikipedia.org/wiki/Idempot%C3%AAncia_de_implica%C3%A7%C3%A3o
http://pt.wikipedia.org/wiki/Gram%C3%A1tica_livre_do_contexto_generalizada
http://pt.wikipedia.org/wiki/Gram%C3%A1tica_de_Cabe%C3%A7a
http://pt.wikipedia.org/wiki/Sequencias_autom%C3%A1ticas
http://pt.wikipedia.org/wiki/FO_%28complexidade%29
http://pt.wikipedia.org/wiki/P/polinomial
http://pt.wikipedia.org/wiki/Linguagem_livre_de_contexto_determin%C3%ADstica
http://pt.wikipedia
.org/wiki/Gram%C3%A1tica_livre_de_contexto_determin%C3%ADstica
http://pt.wikipedia
.org/wiki/Lema_do_bombeamento_para_linguagens_livre_de_contexto
http://pt.wikipedia.org/wiki/Polimorfismo_param%C3%A9trico
http://pt.wikipedia.org/wiki/Aut%C3%B4mato_de_B%C3%BCchi
http://pt.wikipedia.org/wiki/Programa%C3%A7%C3%A3o_orientada_%C3%A0_automatos
http://pt.wikipedia.org/wiki/RE_(complexidade)
http://pt.wikipedia.org/wiki/Redu%C3%A7%C3%A3o_Linear
http://pt.wikipedia.org/wiki/L%C3%B3gica_de_Computabilidade
http://pt.wikipedia.org/wiki/M%C3%A1quina_de_Turing_apenas_de_leitura#Teoria
http://pt.wikipedia
.org/wiki/M%C3%A1quinas_de_Turing_apenas_de_leitura_que_se_movem_apenas_para_direita
http://pt.wikipedia.org/wiki/Programa%C3%A7%C3%A3o_de_Conjunto_de_resposta
http://pt.wikipedia.org/wiki/Gram%C3%A1tica_Indexada
http://pt.wikipedia.org/wiki/Indistinguibilidade_de_Textos_Cifrados
http://pt.wikipedia
.org/wiki/Tabela_de_transi%C3%A7%C3%A3o_de_estados_para_aut%C3%B4matos_finitos
http://pt.wikipedia
.org/wiki/Aut%C3%B4mato_finito_n%C3%A3o-determin%C3%ADstico_com_transi%C3%A7%C3%B5es_%CE%B5
http://pt.wikipedia.org/wiki/Richard_M._Karp
http://pt.wikipedia.org/wiki/Vaughan_Pratt
http://pt.wikipedia.org/wiki/Conectividade_%28teoria_dos_grafos%29
http://pt.wikipedia.org/wiki/Teorema_de_Menger
http://pt.wikipedia.org/wiki/Computa%C3%A7%C3%A3o_Real
http://pt.wikipedia.org/wiki/Teorema_de_Post
http://pt.wikipedia.org/wiki/Conjunto_simples
http://pt.wikipedia
.org/wiki/O_Problema_da_Satisfa%C3%A7%C3%A3o_de_Restri%C3%A7%C3%B5es
http://pt.wikipedia.org/wiki/Satisfa%C3%A7%C3%A3o_de_restri%C3%A7%C3%B5es
http://pt.wikipedia.org/wiki/Estados_(Ci%C3%AAncia_da_Computa%C3%A7%C3%A3o)
http://pt.wikipedia.org/wiki/Lógica_não_classica
http://pt.wikipedia.org/wiki/Lógica_classica
http://pt.wikipedia.org/wiki/Aut%C3%B4mato_Celular_de_Codd
http://pt.wikipedia.org/wiki/Circuitos_Booleanos
http://pt.wikipedia.org/wiki/Certificado_de_Primalidade
http://pt.wikipedia.org/wiki/Turing_switch
http://pt.wikipedia.org/wiki/M%C3%A1quinas_desorganizadas

Re: [Logica-l] Contribuições de alunos do CIn-UFPE à Wikipédia (em português), 2012.2

2013-04-27 Por tôpico Ruy de Queiroz
Dória,


2013/4/27 Francisco Antonio Doria famado...@gmail.com

 Houve algum problema, Ruy, com os editores da Wiki?

Alguns problemas menores, que já foram contornados.

Ruy




 On Sat, Apr 27, 2013 at 5:55 PM, Ruy de Queiroz r...@cin.ufpe.br wrote:

 Seguem os endereços de verbetes da Wikipédia para os quais contribuíram os
 alunos do CIn-UFPE em 2012.2:
 *
 *
 *Lógica*

 http://pt.wikipedia.org/wiki/Verdade_l%C3%B3gica
 http://pt.wikipedia.org/wiki/Begriffsschrift

 http://pt.wikipedia.org/wiki/Modelo_de_aritm%C3%A9tica_n%C3%A3o-padr%C3%A3o
 http://pt.wikipedia.org/wiki/Equival%C3%AAncia_elementar
 http://pt.wikipedia.org/wiki/Segundo_problema_de_Hilbert
 http://pt.wikipedia.org/wiki/Corretude_%28l%C3%B3gica%29
 http://pt.wikipedia.org/wiki/Defini%C3%A7%C3%A3o
 http://pt.wikipedia.org/wiki/L%C3%B3gica_subestrutural
 http://pt.wikipedia.org/wiki/Igualdade_l%C3%B3gica
 http://pt.wikipedia.org/wiki/Satisfatibilidade_de_Horn
 http://pt.wikipedia.org/wiki/Contraposi%C3%A7%C3%A3o
 http://pt.wikipedia.org/wiki/Teorema_da_elimina%C3%A7%C3%A3o_do_corte
 http://pt.wikipedia.org/wiki/Sequente
 http://pt.wikipedia.org/wiki/Tarski%27s_World
 http://pt.wikipedia.org/wiki/Paradoxo_de_Quine
 http://pt.wikipedia.org/wiki/F%C3%B3rmula_bem_formada

 http://pt.wikipedia.org/wiki/Propriedades_de_Normaliza%C3%A7%C3%A3o_(reescrita_abstrata)
 
 http://pt.wikipedia.org/wiki/Propriedades_de_Normaliza%C3%A7%C3%A3o_%28reescrita_abstrata%29
 

 http://pt.wikipedia.org/wiki/C%C3%A1lculo_de_sequentes
 http://pt.wikipedia.org/wiki/Sistema_axiom%C3%A1tico
 http://pt.wikipedia.org/wiki/Axiomas_de_Hilbert
 http://pt.wikipedia.org/wiki/L%C3%B3gica_de_ordem_superior
 http://pt.wikipedia.org/wiki/Aritm%C3%A9tica_primitiva_recursiva
 http://pt.wikipedia.org/wiki/L%C3%B3gica_do_Di%C3%A1logo
 http://pt.wikipedia.org/wiki/Minimiza%C3%A7%C3%A3o_de_Circuitos
 http://pt.wikipedia.org/wiki/Algoritmo_de_Quine-McCluskey
 http://pt.wikipedia.org/wiki/Equissatisfatibilidade
 http://pt.wikipedia.org/wiki/Equiconsistência
 http://pt.wikipedia.org/wiki/Sistema_de_Hilbert
 http://pt.wikipedia.org/wiki/Predicado_(l%C3%B3gica)
 http://pt.wikipedia.org/wiki/Predicado_%28l%C3%B3gica%29
 http://pt.wikipedia.org/wiki/Senten%C3%A7a_(l%C3%B3gica_matem%C3%A1tica)
 http://pt.wikipedia.org/wiki/Senten%C3%A7a_%28l%C3%B3gica_matem%C3%A1tica%29
 
 http://pt.wikipedia.org/wiki/Valora%C3%A7%C3%A3o_(l%C3%B3gica)
 http://pt.wikipedia.org/wiki/Valora%C3%A7%C3%A3o_%28l%C3%B3gica%29

 http://pt.wikipedia.org/wiki/Teoria_dos_tipos_intuicionista
 http://pt.wikipedia.org/wiki/An%C3%A1lise_construtiva
 https://pt.wikipedia.org/wiki/Isomorfismo_de_Curry-Howard


 *Teoria da Computação*

 http://pt.wikipedia.org/wiki/Problema_de_otimiza%C3%A7%C3%A3o
 http://pt.wikipedia.org/wiki/Comutatividade_da_conjun%C3%A7%C3%A3o
 http://pt.wikipedia.org/wiki/Idempot%C3%AAncia_de_implica%C3%A7%C3%A3o
 http://pt.wikipedia.org/wiki/Gram%C3%A1tica_livre_do_contexto_generalizada
 http://pt.wikipedia.org/wiki/Gram%C3%A1tica_de_Cabe%C3%A7a
 http://pt.wikipedia.org/wiki/Sequencias_autom%C3%A1ticas
 http://pt.wikipedia.org/wiki/FO_%28complexidade%29
 http://pt.wikipedia.org/wiki/P/polinomial

 http://pt.wikipedia.org/wiki/Linguagem_livre_de_contexto_determin%C3%ADstica
 http://pt.wikipedia
 .org/wiki/Gram%C3%A1tica_livre_de_contexto_determin%C3%ADstica
 http://pt.wikipedia
 .org/wiki/Lema_do_bombeamento_para_linguagens_livre_de_contexto
 http://pt.wikipedia.org/wiki/Polimorfismo_param%C3%A9trico
 http://pt.wikipedia.org/wiki/Aut%C3%B4mato_de_B%C3%BCchi

 http://pt.wikipedia.org/wiki/Programa%C3%A7%C3%A3o_orientada_%C3%A0_automatos
 http://pt.wikipedia.org/wiki/RE_(complexidade)
 http://pt.wikipedia.org/wiki/Redu%C3%A7%C3%A3o_Linear
 http://pt.wikipedia.org/wiki/L%C3%B3gica_de_Computabilidade

 http://pt.wikipedia.org/wiki/M%C3%A1quina_de_Turing_apenas_de_leitura#Teoria
 http://pt.wikipedia

 .org/wiki/M%C3%A1quinas_de_Turing_apenas_de_leitura_que_se_movem_apenas_para_direita
 http://pt.wikipedia.org/wiki/Programa%C3%A7%C3%A3o_de_Conjunto_de_resposta
 http://pt.wikipedia.org/wiki/Gram%C3%A1tica_Indexada
 http://pt.wikipedia.org/wiki/Indistinguibilidade_de_Textos_Cifrados
 http://pt.wikipedia

 .org/wiki/Tabela_de_transi%C3%A7%C3%A3o_de_estados_para_aut%C3%B4matos_finitos
 http://pt.wikipedia

 .org/wiki/Aut%C3%B4mato_finito_n%C3%A3o-determin%C3%ADstico_com_transi%C3%A7%C3%B5es_%CE%B5
 http://pt.wikipedia.org/wiki/Richard_M._Karp
 http://pt.wikipedia.org/wiki/Vaughan_Pratt
 http://pt.wikipedia.org/wiki/Conectividade_%28teoria_dos_grafos%29
 http://pt.wikipedia.org/wiki/Teorema_de_Menger
 http://pt.wikipedia.org/wiki/Computa%C3%A7%C3%A3o_Real
 http://pt.wikipedia.org/wiki/Teorema_de_Post
 http://pt.wikipedia.org/wiki/Conjunto_simples
 http://pt.wikipedia
 .org/wiki/O_Problema_da_Satisfa%C3%A7%C3%A3o_de_Restri%C3%A7%C3%B5es
 http://pt.wikipedia.org/wiki/Satisfa%C3%A7%C3%A3o_de_restri%C3%A7%C3%B5es

 http://pt.wikipedia.org/wiki/Estados_(Ci%C3%AAncia_da_Computa%C3%A7%C3%A3o)
 http://pt.wikipedia.org/wiki

[Logica-l] E. W. Beth Dissertation Prize: 2013 call for nominations

2013-03-26 Por tôpico Ruy de Queiroz
*E. W. Beth Dissertation Prize: 2013 call for nominations*

Since 2002, FoLLI (the Association for Logic, Language, and Information,
http://institucional.us.es/folliweb/) awards the E.W. Beth Dissertation
Prize to outstanding dissertations in the fields of Logic, Language, and
Information. We invite submissions for the best dissertation which resulted
in a Ph.D. degree in the year 2012. The dissertations will be judged on
technical depth and strength, originality, and impact made in at least two
of three fields of Logic, Language, and Computation. Interdisciplinarity is
an important feature of the theses competing for the E.W. Beth Dissertation
Prize.

Who qualifies.

Nominations of candidates are admitted who were awarded a Ph.D. degree in
the areas of Logic, Language, or Information between January 1st, 2012 and
December 31st, 2012. There is no restriction on the nationality of the
candidate or the university where the Ph.D. was granted. After a careful
consideration, FoLLI has decided to accept only dissertations written in
English. Dissertations produced in 2012 but not written in English or not
translated will be allowed for submission, after translation, also with the
call next year (for dissertations defended in 2013). The present call for
nominations for the E.W. Beth Disertation Award 2013 will also accept
nominations of full English translations of theses originally written in
another language than English and defended in 2011 or 2012.

Prize.

The prize consists of:

-a certificate

-a donation of 2500 euros provided by the E.W. Beth Foundation

-an invitation to submit the thesis (or a revised version of it) to the
FoLLI Publications on Logic, Language and Information (Springer). For
further information on this series see the FoLLI site.

How to submit.

Only electronic submissions are accepted. The following documents are
required:

1. The thesis in pdf format (ps/doc/rtf not accepted);

2. A ten page abstract of the dissertation in pdf format;

3. A letter of nomination from the thesis supervisor. Self-nominations are
not admitted: each nomination must be sponsored by the thesis supervisor.
The letter of nomination should concisely describe the scope and
significance of the dissertation and state when the degree was officially
awarded;

4. Two additional letters of support, including at least one letter from a
referee not affiliated with the academic institution that awarded the Ph.D.
degree.

All documents must be submitted electronically (preferably as a zip file)
to bus...@amu.edu.pl. Hard copy submissions are not admitted. In case of
any problems with the email submission or a lack of notification within
three working days, nominators should write to bus...@amu.edu.pl.

Important dates:

Deadline for Submissions: May 12, 2013.
Notification of Decision: July 14, 2013.

Committee :

Chris Barker (New York)

Wojciech Buszkowski (chair) (Poznan)

Michael Kaminski (Haifa)

Dale Miller (Palaiseau)

Larry Moss (Bloomington)

Ian Pratt-Hartmann (Manchester)

Ruy de Queiroz (Recife)

Giovanni Sambin (Padua)

Rob van der Sandt (Nijmegen)

Rineke Verbrugge (Groningen)

Heinrich Wansing (Bochum)
___
Logica-l mailing list
Logica-l@dimap.ufrn.br
http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l


[Logica-l] WoLLIC 2013 - CFP - DEADLINE APPROACHING

2013-03-15 Por tôpico Ruy de Queiroz
://www.aslonline.org/studenttravelawards.html for details.

*Important Dates*

   - *March 25th, 2013*: Paper title and abstract deadline* *
   - *March 29th, 2013*: Full paper deadline
   - May 3rd, 2013: Author notification
   - May 15th, 2013: Final version deadline (firm)


*Programme Committee*

   - Albert Atserias http://www.lsi.upc.edu/~atserias/ (UPC Barcelona)
   - Alexandru Baltag
http://www.illc.uva.nl/People/show_person.php?Person_id=Baltag+A.B.(Univ
   Amsterdam)
   - Stephanie Delaune  http://www.lsv.ens-cachan.fr/~delaune/(ENS, CNRS)
   - Amy Felty http://www.site.uottawa.ca/~afelty/ (Univ Ottawa)
   - Santiago Figueira http://www.glyc.dc.uba.ar/santiago/ (Univ Buenos
   Aires)
   - Amelie Gheerbrant http://homepages.inf.ed.ac.uk/agheerbr/ (Univ
   Edinburgh)
   - Radha Jagadeesan http://reed.cs.depaul.edu/rjagadeesan/ (DePaul Univ)
   - Delia Kesner http://www.pps.univ-paris-diderot.fr/~kesner/ (Univ
   Paris-Diderot)
   - Benoit Larose http://www.mathstat.concordia.ca/faculty/larose/
(Concordia
   Univ)
   - Leonid Libkin http://homepages.inf.ed.ac.uk/libkin/ (Univ Edinburgh
   - CHAIR)
   - Fenrong Liu http://fenrong.net/ (Tsinghua Univ)
   - Jerzy Marcinkowski http://www.ii.uni.wroc.pl/~jma/ (Wroclaw Univ)
   - Peter O'Hearn http://www0.cs.ucl.ac.uk/staff/p.ohearn/ (UCL)
   - Joël Ouaknine http://www.cs.ox.ac.uk/joel.ouaknine/ (Oxford Univ)
   - Gerald Penn http://www.cs.toronto.edu/~gpenn/ (Univ Toronto)
   - Gabriele Puppis http://www.labri.fr/perso/gpuppis/ (CNRS/LaBRI -
   Univ Bordeaux)
   - R. Ramanujam http://www.imsc.res.in/~jam/ (The Institute of
   Mathematical Sciences)
   - Peter Selinger http://www.mathstat.dal.ca/~selinger/ (Dalhousie Univ)
   - Szymon Torunczyk http://www.mimuw.edu.pl/~szymtor/ (Warsaw Univ)
   - Anna Zamansky  http://www.cs.tau.ac.il/~annaz/(TU Wien)


*Steering Committee*

   - Samson Abramksy, Johan van Benthem, Anuj Dawar, Joe Halpern, Wilfrid
   Hodges, Daniel Leivant, Angus Macintyre, Grigori Mints, Luke Ong, Hiroakira
   Ono, Ruy de Queiroz.


*Organising Committee*

   - Ulrich Kohlenbach http://www.loria.fr/~areces/ (Tech U Darmstadt)
   (Local chair)
   - Anjolina G. de Oliveira http://www.cin.ufpe.br/~ago (U Fed
   Pernambuco)
   - Martin Otto http://www.mathematik.tu-darmstadt.de/~otto/ (Tech U
   Darmstadt)
   - Ruy de Queiroz http://www.cin.ufpe.br/~ruy (U Fed Pernambuco)
   (co-chair)
   - Thomas Streicher http://www.mathematik.tu-darmstadt.de/~streicher/ (Tech
   U Darmstadt)
   - Martin Ziegler http://www.mathematik.tu-darmstadt.de/~ziegler/ (Tech
   U Darmstadt)


*Further information*

Contact one of the Co-Chairs of the Organising Committee.

*Web page*
http://wollic.org/wollic2013/
___
Logica-l mailing list
Logica-l@dimap.ufrn.br
http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l


[Logica-l] Fwd: ICCL Summer School 2013

2013-02-24 Por tôpico Ruy de Queiroz
-- Forwarded message --
From: Bertram Fronhöfer bertram.fronhoe...@tu-dresden.de
Date: 2013/2/24
Subject: ICCL Summer School 2013
To: r...@informatik.uni-leipzig.de, r...@tifr.res.in, rajeev.g...@anu.edu.au,
ranto...@ifi.uio.no, razvan.diacone...@imar.ro, rcign...@2vias.com.ar,
regis.ale...@gmail.com, rends...@gmail.com, r...@math.ist.utl.pt,
rin...@ai.rug.nl, r...@risc.cnrs.fr, rle...@mat.puc.cl, ro...@ens.fr,
ros...@dis.uniroma1.it, ross.br...@latrobe.edu.au, ruff...@gmx.net,
ruleml-...@ruleml.org, r...@cin.ufpe.br, ryan.yo...@anu.edu.au,
r...@linguist.jussieu.fr, rzym...@wp.pl, saliy...@indiana.edu,
salt...@bc4.so-net.ne.jp, s...@ruc.dk, saut...@terra.com.br,
sayady...@yahoo.com, schang.fab...@voila.fr, se...@usal.es,
seman...@rz.uni-duesseldorf.de, seman...@uni-duesseldorf.de,
senseval-disc...@listserv.hum.gu.se, s...@phil.ufl.edu, s...@tut.fi,
shill...@ualberta.ca




ICCL Summer School 2013


As in the past summer schools at the Technische Universität Dresden,
people from distinct, but communicating communities will gather in an
informal and friendly atmosphere. This two-week event is aimed at
graduate students, researchers and practitioners.

The topic of this year's summer school is

Semantic Web - Ontology Languages and Their Use

The summer school is devoted to the Semantic Web, a very dynamic and
current area of research and application which aims at making
information on the World Wide Web fit for intelligent systems
applications. One of the key ideas of the Semantic Web approach is to
make use of methods from knowledge representation and of AI research
in general in order to obtain seamless integration of information from
diverse resources, interoperability of tools, enhance search
functionalities, and the like.

Central for this development is the design of knowledge representation
languages for building so-called ontologies, which serve as a kind of
metadata to describe the semantics or meaning of data on the Web. Of
primary importance are ontology languages and related recommended
standards by the World Wide Web Consortium (W3C), as well as methods
and algorithm for their processing.

The Semantic Web is now an advanced interdisciplinary field having its
home in Computer Science. Third party funding for more than a decade,
in particular from the European Union, has led to significant
progress.  Systems like Apple's Siri or IBM's Watson, adaptions of
Semantic-Web-based technologies for e.g. schema.org, Facebook's Open
Graph or Google's Knowledge Graph bring these technologies to
widespread use and application. Through so-called Linked Data, high
volumes of Semantic-Web-processable data is already available on
the Web.

The ICCL Summer School 2013 will introduce to Semantic Web Ontology
Languages and some of their application areas, and highlight related
research problems.


Registration:

If you want to attend the summer school, we would like you to register
via the Online Registration Form preferably by April 11, 2013. This
deadline is obligatory for all who want to apply for a grant.

After April 11, 2013, registration will be possible as long as there
are vacant places. (Since we intend to restrict participation to about
60 people, in case of excessive demand, we will have to close the
registration to the summer school.)

Please register at the latest by July 1, 2013, because - apart from
the mentioned overall restriction of participation - we would need an
early estimate of the number of participants.

People applying until April 11, 2013, and applying for a grant will be
informed about respective decisions on grants by end of April 2013.

After April 11, 2013 applications for grants cannot be considered
any more.

An on-site check-in is on Sunday, August 18, 2013, at 4 - 7 pm in
room E001 of the Computer Science building. It continues on Monday,
August 19, 2013, 8 - 10 am.


Fees:

(A) We ask for a participation fee of 250 EUR for participants from
the university sector (students, university employees, etc)

(B) We ask for a participation fee of 1000 Euro for participants
from industry.

Please pay this summer school fee in cash at the day of your arrival.

If belonging to the university sector you have to provide some
respective evidence when paying the fees at the check-in (e.g.
student card, web page at a university, etc).



Grants:

A limited number of grants for students and university employees will
be available, which includes a waiver of the participation fee. Please
indicate in your application, if the only possibility for you to
participate is via a grant. Applications for grants must include an
estimate of travel costs. (Such info shall be mentioned in the
respective parts of the online registration form).

Please consult our web pages for further details.

http://www.computational-**logic.org/content/events/iccl-**
ss-2013/index.php?id=24http://www.computational-logic.org/content/events/iccl-ss-2013/index.php?id=24

[Logica-l] Fwd: European Master's Program in Computational Logic

2013-01-17 Por tôpico Ruy de Queiroz
-- Forwarded message --
From: Bertram Fronhöfer bertram.fronhoe...@tu-dresden.de
Date: 2013/1/17
Subject: European Master's Program in Computational Logic
To: r...@informatik.uni-leipzig.de, r...@tifr.res.in, rajeev.g...@anu.edu.au,
ranto...@ifi.uio.no, razvan.diacone...@imar.ro, rcign...@2vias.com.ar,
regis.ale...@gmail.com, rends...@gmail.com, r...@math.ist.utl.pt,
rin...@ai.rug.nl, r...@risc.cnrs.fr, rle...@mat.puc.cl, ro...@ens.fr,
ros...@dis.uniroma1.it, ross.br...@latrobe.edu.au, ruff...@gmx.net,
ruleml-...@ruleml.org, r...@cin.ufpe.br, ryan.yo...@anu.edu.au,
r...@linguist.jussieu.fr, rzym...@wp.pl, saliy...@indiana.edu,
salt...@bc4.so-net.ne.jp, s...@ruc.dk, saut...@terra.com.br,
sayady...@yahoo.com, schang.fab...@voila.fr, se...@usal.es,
seman...@rz.uni-duesseldorf.de, seman...@uni-duesseldorf.de,
senseval-disc...@listserv.hum.gu.se, s...@phil.ufl.edu, s...@tut.fi,
shill...@ualberta.ca




Dear all,

I'd like to draw your attention to the fact that fresh Erasmus Mundus
scholarships are available for Non-European AND European students who
enroll in our European Master's Program in Computational Logic in the fall
of 2013. The deadline for application is 31 January, 2013. More details are
given below. In particular, I'd like to draw your attention to the fact
that we are able to provide grants to EU-students for doing their project
at the National ICT of Australia (NICTA).

Please spread this information as wide as possible among friends and
colleagues, at your old universities and the places, where you currently
live and work.

Many thanks -- Steffen


*
The European Master's Program in Computational Logic

We are glad to announce to you the possibility to join our European
Master's Program of Computational Logic. This program is offered jointly at
the Free-University of Bozen-Bolzano in Italy, the Technische Universität
Dresden in Germany, the Universidade Nova de Lisboa in Portugal and the
Technische Universität Wien in Austria. Within this program you have the
choice to study at two /three of the four European universities. In
addition, you can do your project work at the National ICT of Australia
(NICTA). You will graduate with a MSc in Computer Science and obtain a
joint degree. Information on the universities and the program including the
application procedure is provided here:

http://www.emcl-study.eu/home.**html http://www.emcl-study.eu/home.html

Language of instruction is English. Tuition fees are 3.000 EUR (for
non-European students) and 1.000 (for European students) per year.

We would like to draw your attention to the ERASMUS-MUNDUS scholarship
program. The ERASMUS-MUNDUS consortium offers 2-year scholarships up to
 48.000 EUR for non-EU students and up to 23.000 EUR for EU students of our
European Master's Program in Computational Logic.

More information on the scholarship program is available from:

http://www.emcl-study.eu/**fileadmin/emcl_booklet_tree/**ma_em_grant.htmlhttp://www.emcl-study.eu/fileadmin/emcl_booklet_tree/ma_em_grant.html

Do not hesitate to contact us  if you have any further questions.

Kind regards -- Steffen Hölldobler

Prof. Dr. Steffen Hoelldobler
International Center for Computational Logic
Technische Universität Dresden
01062 Dresden, Germany

phone: [+49](351)46 33 83 40
fax: [+49](351)46 33 83 42
email: s...@iccl.tu-dresden.de

-- 

Dr.rer.nat.habil. Bertram Fronhöfer
TU Dresden
Department of Computer Science
International Center for Computational Logic
01062 Dresden, Germany
Tel.: +49 (0)351 463 39095
___
Logica-l mailing list
Logica-l@dimap.ufrn.br
http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l


Re: [Logica-l] Summer School in Jan/Feb 2013

2013-01-03 Por tôpico Ruy de Queiroz
Confirmados dias, horários e salas do mini-curso de Michael Warren
(Princeton) no Programa de Verão da DMAT-UFPE
2013http://www.dmat.ufpe.br/~verao2013/
:

28/01   14h-18h   Anfiteatro do Centro de Informática
29/01   15h-18h   Anfiteatro do Centro de Informática
30/01   14h-18h   Anfiteatro do Centro de Informática
31/01   14h-18h   Auditório (1o. andar) do Centro de Informática
01/02   14h-18h   Anfiteatro do Centro de Informática


Aproveito para indicar a leitura de um artigo de Michael Warren, justamente
sobre o tópico do mini-curso de verão.

Ruy

P.S. Para quaisquer informações sobre o Programa de Verão DMAT 2013, visite
http://www.dmat.ufpe.br/~verao2013/



Homotopy type theory and Voevodsky's univalent
foundationshttp://arxiv.org/abs/1210.5658
Álvaro Pelayo http://arxiv.org/find/math/1/au:+Pelayo_A/0/1/0/all/0/1,
Michael
A. Warren http://arxiv.org/find/math/1/au:+Warren_M/0/1/0/all/0/1
(Submitted on 20 Oct 2012)

Recent discoveries have been made connecting abstract homotopy theory and
the field of type theory from logic and theoretical computer science. This
has given rise to a new field, which has been christened homotopy type
theory. In this direction, Vladimir Voevodsky observed that it is possible
to model type theory using simplicial sets and that this model satisfies an
additional property, called the Univalence Axiom, which has a number of
striking consequences. He has subsequently advocated a program, which he
calls univalent foundations, of developing mathematics in the setting of
type theory with the Univalence Axiom and possibly other additional axioms
motivated by the simplicial set model. Because type theory possesses good
computational properties, this program can be carried out in a computer
proof assistant. In this paper we give an introduction to homotopy type
theory in Voevodsky's setting, paying attention to both theoretical and
practical issues. In particular, the paper serves as an introduction to
both the general ideas of homotopy type theory as well as to some of the
concrete details of Voevodsky's work using the well-known proof assistant
Coq. The paper is written for a general audience of mathematicians with
basic knowledge of algebraic topology; the paper does not assume any
preliminary knowledge of type theory, logic, or computer science.

Comments:48 pages, 14 figuresSubjects:Logic (math.LO); Logic in Computer
Science (cs.LO); Algebraic Topology (math.AT)Cite
as:arXiv:1210.5658http://arxiv.org/abs/1210.5658
 [math.LO] (or arXiv:1210.5658v1 http://arxiv.org/abs/1210.5658v1
 [math.LO] for this version)

2012/12/3 Ruy de Queiroz r...@cin.ufpe.br

 Caros,

 Estamos trazendo Michael Warren http://www.math.ias.edu/~mwarren/, do
 Institute of Advanced Study, Princeton, (da equipe de Vladimir Voevodsky),
 para ministrar um mini-curso de Homotopy Type Theory no Programa de Verão
 da Matemática da UFPE de 2013, a ser realizado no periodo de 28/01 a 02/02.

 Esperamos contar com a presença de todos os interessados no tema.

 Abraço,
 Ruy
 --


 TITLE:

 Types and homotopy types

 ABSTRACT:

 In this series of lectures I will give an introduction to recent research
 in what has been called homotopy type theory and to Voevodsky's
 univalent foundations program.  Both of these areas of research involve
 connections between homotopy theory, higher-dimensional category theory and
 type theory, and we aim to introduce sufficient background in all of these
 areas for attendees to appreciate these connections.  Particular attention
 will be paid to issues related to proving results in homotopy theory in
 this setting including the question of how to represent spaces as datatypes.

 BIO:

 Dr. Warren completed his Ph.D. thesis, entitled Homotopy Theoretic
 Aspects of Constructive Type Theory and supervised by Prof. Steven Awodey,
 at Carnegie Mellon University in 2008. He was then a Fields Institute
 Postdoctoral Fellow at the University of Ottawa, where he was a member of
 the Logic and Foundations of Computing Group, from 2008 to 2010. During the
 2010 academic year he was an AARMS Postdoctoral Fellow working in
 the Atlantic Category Theory Group at Dalhousie University.  Since 2011 he
 has been a Member of the School of Mathematics at the Institute for
 Advanced Study.  His research is in the areas of category theory,
 mathematical logic, algebraic topology, and theoretical computer science.
 -






___
Logica-l mailing list
Logica-l@dimap.ufrn.br
http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l


Re: [Logica-l] Publicação da tradução de A Shorter Model Theory, Wilfrid Hodges

2012-12-30 Por tôpico Ruy de Queiroz
O livro já pode ser adquirido no portal da Amazon.com:

http://www.amazon.com/Vers%C3%A3o-Curta-Teoria-Modelos-Portuguese/dp/1848900953/ref=sr_1_7?s=booksie=UTF8qid=1356885496sr=1-7keywords=wilfrid+hodges

Feliz 2013!

Ruy

Em 23 de dezembro de 2012 15:11, Ruy de Queiroz r...@cin.ufpe.br escreveu:

 A College Publications assinala a publicação da tradução do livro A
 Shorter Model Theory (Cambridge Univ Press, 1997), em 17/Dezembro/2012,
 como Vol. 3 da Série Cadernos de Lógica e Computação (dirigida por
 Amílcar Sernadas  Cristina Sernadas): (
 http://www.collegepublications.co.uk/clc/?3)

 *Cadernos de Lógica e Computação, Vol. 3*
 *Uma Versão Mais Curta de Teoria dos Modelos*

 *Wilfrid Hodges. Traduzido por Ruy J. G. B. de Queiroz*

 Eis um livro-texto atualizado de teoria de modelos levando o leitor das
 primeiras definições até o teorema de Morley e as partes elementares da
 teoria da estabilidade. Além dos resultados padrão tais como os teoremas da
 compacidade e da omissão de tipos, o livro também descreve várias conexões
 com a álgebra, incluindo o método de eliminação de quantificadores de
 Skolem-Tarski, modelo-completude, grupos de automorfismos e
 omega-categoricidade, ultraprodutos, O-minimalidade e estruturas de posto
 de Morley finito. O material sobre equivalências vai-e-vem, interpretaões e
 leis zero-um podem servir como introdução a aplicações de teoria de modelos
 à ciência da computação. Cada capítulo termina com um breve comentário
 sobre a literatura e sugestões de leitura adicional.


 17 December 2012

 978-1-84890-095-0

___
Logica-l mailing list
Logica-l@dimap.ufrn.br
http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l


[Logica-l] WoLLIC 2013 (Darmstadt) - 2nd Call for Papers

2012-12-24 Por tôpico Ruy de Queiroz
   - May 3rd, 2013: Author notification
   - May 15th, 2013: Final version deadline (firm)


*Programme Committee*

   - Albert Atserias http://www.lsi.upc.edu/~atserias/ (UPC Barcelona)
   - Alexandru Baltag
http://www.illc.uva.nl/People/show_person.php?Person_id=Baltag+A.B.(Univ
   Amsterdam)
   - Stephanie Delaune  http://www.lsv.ens-cachan.fr/~delaune/(ENS, CNRS)
   - Amy Felty http://www.site.uottawa.ca/~afelty/ (Univ Ottawa)
   - Santiago Figueira http://www.glyc.dc.uba.ar/santiago/ (Univ Buenos
   Aires)
   - Amelie Gheerbrant http://homepages.inf.ed.ac.uk/agheerbr/ (Univ
   Edinburgh)
   - Radha Jagadeesan http://reed.cs.depaul.edu/rjagadeesan/ (DePaul Univ)
   - Delia Kesner http://www.pps.univ-paris-diderot.fr/~kesner/ (Univ
   Paris-Diderot)
   - Benoit Larose http://www.mathstat.concordia.ca/faculty/larose/
(Concordia
   Univ)
   - Leonid Libkin http://homepages.inf.ed.ac.uk/libkin/ (Univ Edinburgh
   - CHAIR)
   - Fenrong Liu http://fenrong.net/ (Tsinghua Univ)
   - Jerzy Marcinkowski http://www.ii.uni.wroc.pl/~jma/ (Wroclaw Univ)
   - Peter O'Hearn http://www0.cs.ucl.ac.uk/staff/p.ohearn/ (UCL)
   - Joël Ouaknine http://www.cs.ox.ac.uk/joel.ouaknine/ (Oxford Univ)
   - Gerald Penn http://www.cs.toronto.edu/~gpenn/ (Univ Toronto)
   - Gabriele Puppis http://www.labri.fr/perso/gpuppis/ (CNRS/LaBRI -
   Univ Bordeaux)
   - R. Ramanujam http://www.imsc.res.in/~jam/ (The Institute of
   Mathematical Sciences)
   - Peter Selinger http://www.mathstat.dal.ca/~selinger/ (Dalhousie Univ)
   - Szymon Torunczyk http://www.mimuw.edu.pl/~szymtor/ (Warsaw Univ)
   - Anna Zamansky  http://www.cs.tau.ac.il/~annaz/(TU Wien)


*Steering Committee*

   - Samson Abramksy, Johan van Benthem, Anuj Dawar, Joe Halpern, Wilfrid
   Hodges, Daniel Leivant, Angus Macintyre, Grigori Mints, Luke Ong, Hiroakira
   Ono, Ruy de Queiroz.


*Organising Committee*

   - Ulrich Kohlenbach http://www.loria.fr/~areces/ (Tech U Darmstadt)
   (Local chair)
   - Anjolina G. de Oliveira http://www.cin.ufpe.br/~ago (U Fed
   Pernambuco)
   - Martin Otto http://www.mathematik.tu-darmstadt.de/~otto/ (Tech U
   Darmstadt)
   - Ruy de Queiroz http://www.cin.ufpe.br/~ruy (U Fed Pernambuco)
   (co-chair)
   - Thomas Streicher http://www.mathematik.tu-darmstadt.de/~streicher/ (Tech
   U Darmstadt)
   - Martin Ziegler http://www.mathematik.tu-darmstadt.de/~ziegler/ (Tech
   U Darmstadt)


*Further information*
Contact one of the Co-Chairs of the Organising Committee.

*Web page*
http://wollic.org/wollic2013/
___
Logica-l mailing list
Logica-l@dimap.ufrn.br
http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l


[Logica-l] Publicação da tradução de A Shorter Model Theory, Wilfrid Hodges

2012-12-23 Por tôpico Ruy de Queiroz
A College Publications assinala a publicação da tradução do livro A
Shorter Model Theory (Cambridge Univ Press, 1997), em 17/Dezembro/2012,
como Vol. 3 da Série Cadernos de Lógica e Computação (dirigida por
Amílcar Sernadas  Cristina Sernadas): (
http://www.collegepublications.co.uk/clc/?3)

*Cadernos de Lógica e Computação, Vol. 3*
*Uma Versão Mais Curta de Teoria dos Modelos*

*Wilfrid Hodges. Traduzido por Ruy J. G. B. de Queiroz*

Eis um livro-texto atualizado de teoria de modelos levando o leitor das
primeiras definições até o teorema de Morley e as partes elementares da
teoria da estabilidade. Além dos resultados padrão tais como os teoremas da
compacidade e da omissão de tipos, o livro também descreve várias conexões
com a álgebra, incluindo o método de eliminação de quantificadores de
Skolem-Tarski, modelo-completude, grupos de automorfismos e
omega-categoricidade, ultraprodutos, O-minimalidade e estruturas de posto
de Morley finito. O material sobre equivalências vai-e-vem, interpretaões e
leis zero-um podem servir como introdução a aplicações de teoria de modelos
à ciência da computação. Cada capítulo termina com um breve comentário
sobre a literatura e sugestões de leitura adicional.


17 December 2012

978-1-84890-095-0
___
Logica-l mailing list
Logica-l@dimap.ufrn.br
http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l


[Logica-l] Fwd: New PhD Program in Pure and Applied Logic (ATTN: undergrads)

2012-10-18 Por tôpico Ruy de Queiroz
-- Forwarded message --
From: Jeremy Avigad avi...@cmu.edu
Date: Thu, Oct 18, 2012 at 4:30 PM
Subject: New PhD program in Pure and Applied Logic
To:



Dear colleagues,

The Department of Philosophy at Carnegie Mellon University is now offering
a *Ph.D. in Pure and Applied Logic* as a new track in our PhD program.
There isn't time to update our web pages for the current application
season, so I am asking you to forward this information to students who may
be interested.

The new program is designed to train students for research careers in
mathematical logic and computer science, in areas such as computability
theory, proof theory, categorical logic, automated reasoning, formal
verification, and the semantics of computation. Students in the program
earn an MS from the Department of Mathematical Sciences at Carnegie Mellon,
in addition to writing a dissertation in logic.

The program reflects the interdisciplinary nature of our department. Our
faculty have placed students in positions in mathematics, statistics, and
computer science, and the new program aims to better support these career
paths. Prospective students can simultaneously apply to the Department of
Mathematical Sciences and, if admitted to both programs, make a decision
based on their specific interests.

I would be glad to answer any questions about the new program.

Thanks, and best wishes,

Jeremy



--++**==--++**==--++**==--++**==--++**==--++**==--++**==
logical-methods mailing list
logical-meth...@lists.stanford.edu
https://mailman.stanford.edu/mailman/listinfo/logical-methods
___
Logica-l mailing list
Logica-l@dimap.ufrn.br
http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l


Re: [Logica-l] 50o aniversário de E. Hermann Haeusler

2012-09-25 Por tôpico Ruy de Queiroz
Parabéns a Hermann e aos organizadores dessa bela homenagem!

Ruy

Em 24 de setembro de 2012 16:06, Edward Hermann
edward.haeus...@gmail.comescreveu:


Obrigado Décio !   Valeu    A coisa já está braba tem um
 tempinho…...



 On 5   jan  2009, at 3:02 PM, Décio Krause deciokra...@gmail.com wrote:

  Caro Hermann
  Parabéns e felicidades, e aguente firme que a coisa vai começar a ficar
 braba...
  Ah ah. Felicidades, meu chapa.
  Décio
 
 
  --
  Décio Krause
  Departamento de Filosofia
  Universidade Federal de Santa Catarina
  88040-900 Florianópolis - SC - Brasil
  http://www.cfh.ufsc.br/~dkrause
  --
 
  Em 23/09/2012, às 11:48, Walter Carnielli walter.carnie...@gmail.com
 escreveu:
 
  Parabéns caro Hermann, seja bem vindo ao segundo tercco da sua vida :-)
 
  Abs,
  Waltet
  Em 22/09/2012 20:31, Christiano Braga cbr...@ic.uff.br escreveu:
 
  Pessoal,
 
  no sábado 29/09/12, a partir das 14 h, celebraremos o 50o aniversário
 do
  Prof. Edward Hermann Haeusler, o Hermann, no auditório do RDC na
 PUC-Rio.
 
  A celebração, cujo programa pode ser acessado em
  http://www.ic.uff.br/~cbraga/hermann50/, ocorrerá em paralelo ao 7th
  Logical and Semantic Frameworks with Applications (LSFA 11). Aqueles
 que
  desejarem participar do evento social conjunto do LSFA e Hermann50
 deverão
  se inscrever no LSFA em http://www.uff.br/lsfa.
 
  Saudações,
 
  Christiano
 
  ___
  Logica-l mailing list
  Logica-l@dimap.ufrn.br
  http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l
 
  ___
  Logica-l mailing list
  Logica-l@dimap.ufrn.br
  http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l

 ___
 Logica-l mailing list
 Logica-l@dimap.ufrn.br
 http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l

___
Logica-l mailing list
Logica-l@dimap.ufrn.br
http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l


[Logica-l] WoLLIC 2013 (Darmstadt) - CFP

2012-09-24 Por tôpico Ruy de Queiroz
://homepages.inf.ed.ac.uk/agheerbr/ (Univ
   Edinburgh)
   - Radha Jagadeesan http://reed.cs.depaul.edu/rjagadeesan/ (DePaul Univ)
   - Delia Kesner http://www.pps.univ-paris-diderot.fr/~kesner/ (Univ
   Paris-Diderot)
   - Benoit Larose http://www.mathstat.concordia.ca/faculty/larose/
(Concordia
   Univ)
   - Leonid Libkin http://homepages.inf.ed.ac.uk/libkin/ (Univ Edinburgh
   - CHAIR)
   - Fenrong Liu http://fenrong.net/ (Tsinghua Univ)
   - Jerzy Marcinkowski http://www.ii.uni.wroc.pl/~jma/ (Wroclaw Univ)
   - Peter O'Hearn http://www0.cs.ucl.ac.uk/staff/p.ohearn/ (UCL)
   - Joël Ouaknine http://www.cs.ox.ac.uk/joel.ouaknine/ (Oxford Univ)
   - Gerald Penn http://www.cs.toronto.edu/~gpenn/ (Univ Toronto)
   - Gabriele Puppis http://www.labri.fr/perso/gpuppis/ (CNRS/LaBRI -
   Univ Bordeaux)
   - R. Ramanujam http://www.imsc.res.in/~jam/ (The Institute of
   Mathematical Sciences)
   - Peter Selinger http://www.mathstat.dal.ca/~selinger/ (Dalhousie Univ)
   - Szymon Torunczyk http://www.mimuw.edu.pl/~szymtor/ (Warsaw Univ)
   - Anna Zamansky  http://www.cs.tau.ac.il/~annaz/(TU Wien)


*Steering Committee*

   - Samson Abramksy, Johan van Benthem, Anuj Dawar, Joe Halpern, Wilfrid
   Hodges, Daniel Leivant, Angus Macintyre, Grigori Mints, Luke Ong, Hiroakira
   Ono, Ruy de Queiroz.


*Organising Committee*

   - Ulrich Kohlenbach http://www.loria.fr/~areces/ (Tech U Darmstadt)
   (Local chair)
   - Anjolina G. de Oliveira http://www.cin.ufpe.br/~ago (U Fed
   Pernambuco)
   - Martin Otto http://www.mathematik.tu-darmstadt.de/~otto/ (Tech U
   Darmstadt)
   - Ruy de Queiroz http://www.cin.ufpe.br/~ruy (U Fed Pernambuco)
   (co-chair)
   - Thomas Streicher http://www.mathematik.tu-darmstadt.de/~streicher/ (Tech
   U Darmstadt)
   - Martin Ziegler http://www.mathematik.tu-darmstadt.de/~ziegler/ (Tech
   U Darmstadt)


*Further information*
Contact one of the Co-Chairs of the Organising Committee.

*Web page*
http://wollic.org/wollic2013/
___
Logica-l mailing list
Logica-l@dimap.ufrn.br
http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l


[Logica-l] Cadernos de Lógica e Computação (College Publications)

2012-09-17 Por tôpico Ruy de Queiroz
Nova série de livros em português publicada pela College Publications
(King's College London): *Cadernos em Lógica e Computação*.

Segundo seus coordenadores Amílcar Sernadas e Cristina Sernadas:

Esta série visa facultar aos estudantes universitários dos países de
língua oficial portuguesa bons livros de texto em português, a preços
acessíveis, no domínio lato da lógica e computação, incluindo
traduções de livros já publicados pela College Publications e outros,
bem como textos oriundos das comunidades universitárias destes países.


Está confirmada a publicação de nossa tradução brasileira do livro *A
Shorter Model Theory*, de Wilfrid Hodges, Cambridge U Press, 1997.

Ruy

--

*Cadernos de Lógica e Computação*


Série dirigida por *Amílcar Sernadas  Cristina Sernadas*
Series edited by *Amílcar Sernadas  Cristina Sernadas*


*Cadernos de Lógica e Computação *é uma série de livros em Português que
abrange os domínios da Lógica e da Ciência da Computação e que inclui
livros de texto universitários e monografias de investigação. Os livros de
texto resultam da experiência de ensino universitário de graduação ou
pós-graduação dos seus autores. As monografias de investigação focam
tópicos mais avançados em estilo ainda acessível.

*Cadernos de Lógica e Computação *is a series of books in Portuguese that
covers the full spectrum of the fields of Logic and Computer Science,
including university textbooks and research monographs. Textbooks are
written from class-tested material developed by the authors for
undergraduate or graduate students. Research monographs focus on more
advanced topics but still in accessible style to newcomers.

Comissão Científica
Scientific Committee

Walter Carnielli, Universidade de Campinas
Fernando Ferreira, Universidade de Lisboa
José Luiz Fiadeiro, University of London
Marcelo Finger, Universidade de São Paulo
Denis Hirschfeldt, University of Chicago
Valeria de Paiva, University of Birmingham
Luís Moniz Pereira, Universidade Nova de Lisboa
Ruy de Queiroz, Universidade Federal de Pernambuco
Paulo Oliva, University of London
___
Logica-l mailing list
Logica-l@dimap.ufrn.br
http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l


Re: [Logica-l] Fwd: Walter Carnielli: indicação para medalha de ouro

2012-08-01 Por tôpico Ruy de Queiroz
Parabéns, Walter!

Em 1 de agosto de 2012 13:50, Joao Marcos botoc...@gmail.com escreveu:

-- Forwarded message --
 From: Juliana Bueno-Soler juliana.bu...@cle.unicamp.br
 Date: 2012/8/1
 Subject: Walter Carnielli: indicação para medalha de ouro


 Caros colegas e amigos:

 escrevo para comunicar que o Prof. Walter Carnielli foi indicado para
 receber a medalha de ouro da Telesio Galilei Academy of Science (baseada
 em Bellinzona, Suiça) para 2013 na área de Matemática, por suas
 contribuições conjuntas à Matematica, Lógica e Filosofia

 http://telesio-galilei.com/tg/index.php/academy-award-2013

 O nome da academia homenageia Bernardino Telesio e Galileo Galilei, tidos
 como heróis da resistência à autoridade contra a ciência livre.

 A academia premiou desde 2008 diversos físicos, matemáticos e alguns
 poucos filósofos, incluindo os brasileiros Fernando Galembeck (Química,
 Unicamp) e Djairo Guedes de Figueiredo (Matemática, Unicamp).

 Gostaria que alguém postasse esta mensagem na Lista dos Lógicos
 Brasileiros (da qual eu não faço parte mais).

 Att.,
 Juliana

 +
 Juliana Bueno-Soler
 Professor Adjunto I
 Universidade Federal do ABC - CCNH
 Rua Santa Adélia, 166 - Bangu
 Santo André - SP
 homepages: http://tinyurl.com/juliana-bueno-soler
http://geocities.com/j_bueno13/
 ___
 Logica-l mailing list
 Logica-l@dimap.ufrn.br
 http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l

___
Logica-l mailing list
Logica-l@dimap.ufrn.br
http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l


Re: [Logica-l] weakening theorem - tradução(?); mais comentários

2012-07-31 Por tôpico Ruy de Queiroz
Caro Chico,

Tuas considerações são pertinentes, mas permita-me discordar das
conclusões: o sentido da regra em questão é o de enfraquecer um argumento,
como bem disse Valéria. Daí, é natural que a tradução em português utilize
a palavra enfraquecimento. Aliás, tenho a impressão de que o termo já
está razoavelmente consolidado, tal qual a terminologia teoria da prova.
Não vejo nada de errado em qualquer das duas formas de expressão no
português.

Abraço,
Ruy

Em 31 de julho de 2012 03:27, Francisco Miraglia mirag...@ime.usp.brescreveu:

 Car@s Colegas,

 A mensagem anterior (talvez) tenha sido um pouco críptica e adiciono mais
 alguns comentários:

 1. Traduções precisam levar em conta a sintaxe, denotação e conotação das
 palavras e/ou expressões na língua original. Weakening é a substantivação
 de um gerúndio, algo comum em ingles (mas não em portugues); a
 substantivação
 permanece carregando a conotação de ação, enquanto que enfraquecimento,
 como todo substantivo na língua portuguesa é passivo. Por outro lado,
 parece-me
 que enfraquecendo está longe de satisfatório...

 2. O conteúdo do enunciado (utilizando o que aprendi em uma conferência e
 conversa, ambas ótimas,  com Dag Prawitz em Paris há algum tempo) seria (as
 palavras foram escolhidas com o devido cuidado)

 Se há uma corroboração de P, então qualquer extensão (finita) desta
 corroboração permanece sendo uma corroboração de P.

 3. Para um working mathematician, dependendo de como isto é enunciado,
 pode
 parecer meio estranho: se C = P_1 + P_2 +  + P_n é uma corroboração de
 P,
 i.e.

  C = P_ 1 + P_2 + ... + P_n  P

 então para todo Q

C + Q = P_1 + P_2 +  + P_n + Q  P,

 ou seja, na presença de uma corroboração de P, toda Q é infinitesimal em
 relação a P; na realidade, toda corroboração de P seria infitesimal em
 relação a P (algo como way below vem imediatamente a mente).

 Será que há matemática e lógica interessantes em estudar estas ordens?

 Desnecessário dizer que ordens não arquimedianas (as únicas com
 infinitesimais) são crucais no estudo da teoria fina de corpos, anéis e em
 Valuation Theory em geral.

 Será que existem análogos de valuations e/ou places em lógica,
 reticulados distributivos, álgebras de Heyting, Brouwer ou de Boole (estas,
 como é sabido há tempos, com estrutura natural e interdefinível com uma
 única de anel commutativo com unidade). Será que estas idéias poderiam
 ajudar
 a entender lógicas, suas propriedades, semânticas e sintaxe?

 4. A pergunta original foi muito produtiva; haveria mais a comentar, mas
 fico
 por aqui, enviando a todos

Um grande abraço,

   Chico Miraglia
 __**_
 Logica-l mailing list
 Logica-l@dimap.ufrn.br
 http://www.dimap.ufrn.br/cgi-**bin/mailman/listinfo/logica-lhttp://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l

___
Logica-l mailing list
Logica-l@dimap.ufrn.br
http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l


[Logica-l] Contribuições de alunos do CIn-UFPE à Wikipédia (em português)

2012-07-08 Por tôpico Ruy de Queiroz
Seguem os endereços de verbetes da Wikipédia para os quais contribuíram os
alunos do CIn-UFPE em 2012.1:
*
*
*Lógica*
http://pt.wikipedia.org/wiki/Endomorfismo
http://pt.wikipedia.org/wiki/Axiomas_de_Peano
http://pt.wikipedia.org/wiki/Programa_de_Hilbert
http://pt.wikipedia.org/wiki/Problema_da_generalidade_m%C3%BAltipla
http://pt.wikipedia.org/wiki/Regra_geral_de_Leibniz
http://pt.wikipedia.org/wiki/Conectivos_l%C3%B3gicos
http://pt.wikipedia.org/wiki/Fun%C3%A7%C3%A3o_de_Ackermann
http://pt.wikipedia.org/wiki/Fun%C3%A7%C3%B5es_recursivas_primitivas
http://pt.wikipedia.org/wiki/L%C3%B3gica_de_Hoare
http://pt.wikipedia.org/wiki/Sistema_formal
http://pt.wikipedia.org/wiki/Propaga%C3%A7%C3%A3o_de_unidade
http://pt.wikipedia.org/wiki/Charadas_de_Smullyan
http://pt.wikipedia.org/wiki/Senten%C3%A7a_at%C3%B4mica
http://pt.wikipedia.org/wiki/Conjuntos_Livremente_Gerados
http://pt.wikipedia.org/wiki/Language,_proof_and_logic
http://pt.wikipedia.org/wiki/Prenex
http://pt.wikipedia.org/wiki/Homomorfismo
http://pt.wikipedia.org/wiki/Defini%C3%A7%C3%B5es_da_L%C3%B3gica
http://pt.wikipedia.org/wiki/Grupo_livre
http://pt.wikipedia.org/wiki/Teorema_da_compacidade
http://pt.wikipedia.org/wiki/Subestrutura
http://pt.wikipedia.org/wiki/Conjunto_gerador_de_um_grupo
http://pt.wikipedia.org/wiki/Consist%C3%AAncia_l%C3%B3gica
http://pt.wikipedia.org/wiki/L%C3%B3gica_de_predicados
http://pt.wikipedia.org/wiki/Infer%C3%AAncia
http://pt.wikipedia.org/wiki/Teorema_L%C3%B6wenheim%E2%80%93Skolem

*Teoria da Computação*
http://pt.wikipedia.org/wiki/Máquinas_de_Turing_equivalentes
http://pt.wikipedia.org/wiki/Redução_em_espaço_logar%C3%ADtmicohttp://pt.wikipedia.org/wiki/Redu%C3%A7%C3%A3o_em_espa%C3%A7o_logar%C3%ADtmico
http://pt.wikipedia.org/wiki/Ci%C3%AAncia_da_computa%C3%A7%C3%A3o_te%C3%B3rica
http://pt.wikipedia.org/wiki/Cadeia_vazia
http://pt.wikipedia.org/wiki/Reconhecedores
http://pt.wikipedia.org/wiki/Problema_transcomputacional
http://pt.wikipedia.org/wiki/Turing_tarpit
http://pt.wikipedia.org/wiki/Gregory_Chaitin
http://pt.wikipedia.org/wiki/Julia_Robinson
http://pt.wikipedia.org/wiki/Problema_do_caminho_hamiltoniano
http://pt.wikipedia.org/wiki/Lista_de_problemas_indecidíveis
http://pt.wikipedia.org/wiki/Máquina_de_Turing_de_Várias_Faixas
http://pt.wikipedia.org/wiki/Predicado_T_de_Kleene
http://pt.wikipedia.org/wiki/Hierarquia_de_Crescimento_Lento
http://pt.wikipedia.org/wiki/Teoria_dos_aut%C3%B4matos
http://pt.wikipedia.org/wiki/Salto_de_Turing
http://pt.wikipedia.org/wiki/Fun%C3%A7%C3%A3o_recursiva_primitiva
http://pt.wikipedia.org/wiki/Description_number
http://pt.wikipedia.org/wiki/Teorema_de_hierarquia_de_espaço
http://pt.wikipedia.org/wiki/Teorema_de_hierarquia_de_tempo
http://pt.wikipedia.org/wiki/Teorema_de_craig
http://pt.wikipedia.org/wiki/Redu%C3%A7%C3%A3o_muitos_pra_um
http://pt.wikipedia.org/wiki/Computa%C3%A7%C3%A3o_no_limite
http://pt.wikipedia.org/wiki/M%C3%A1quina_de_Turing_Alternante
http://pt.wikipedia.org/wiki/Maquinas_de_Turing_somente_de_leitura_e_movimentos_%C3%A0_direita
http://pt.wikipedia.org/wiki/Sistema_de_produção_(ciência_da_computação)
http://pt.wikipedia.org/wiki/M%C3%A1quina_de_Turing_Qu%C3%A2ntica
http://pt.wikipedia.org/wiki/M%C3%A1quina_de_Turing_probabil%C3%ADstica
http://pt.wikipedia.org/wiki/M%C3%A1quina_de_Turing_somente_de_leitura
http://pt.wikipedia.org/wiki/Aut%C3%B4mato_com_fila
http://pt.wikipedia.org/wiki/Redu%C3%A7%C3%A3o_em_espa%C3%A7o_logar%C3%ADtmico
http://pt.wikipedia.org/wiki/Sharp-SAT
http://pt.wikipedia.org/wiki/Geografia_Generalizada
http://pt.wikipedia.org/wiki/D%C3%A9cimo_problema_de_Hilbert
http://pt.wikipedia.org/wiki/M%C3%A1quinas_de_Turing_Sim%C3%A9tricas
http://pt.wikipedia.org/wiki/Configura%C3%A7%C3%A3o_de_Grafos
http://pt.wikipedia.org/wiki/Aut%C3%B4matos_%CF%89
http://pt.wikipedia.org/wiki/Grau_de_Turing
http://pt.wikipedia.org/wiki/S%C3%ADmbolos_terminais_e_n%C3%A3o-terminais
http://pt.wikipedia.org/wiki/Transdutor_de_espaço_logarítmico_(LST)
http://pt.wikipedia.org/wiki/Algoritmos_de_Aproximação
http://pt.wikipedia.org/wiki/Máquina_Wang-b
http://pt.wikipedia.org/wiki/Galeria_das_M%C3%A1quinas_de_Turing
http://pt.wikipedia.org/wiki/Turmite
http://pt.wikipedia.org/wiki/Ficheiro:M%C3%A1quina_de_Turing_Mec%C3%A2nica.jpg
http://pt.wikipedia.org/wiki/Ficheiro:M%C3%A1quina_de_Turing_por_Stone.jpg
http://pt.wikipedia.org/wiki/Teorema_da_dicotomia_de_Schaefer
http://pt.wikipedia.org/wiki/3SAT_um_em_tr%C3%AAs
http://pt.wikipedia.org/wiki/Conjuntos_criativos_e_produtivos
http://pt.wikipedia.org/wiki/M%C3%A1quina_de_Turing_universal.
http://pt.wikipedia.org/wiki/Teorema_da_recursividade_de_Kleene
http://pt.wikipedia.org/wiki/Algoritmo_de_Markov
http://pt.wikipedia.org/wiki/Gram%C3%A1tica_irrestrita

*Teoria dos Conjuntos*
http://pt.wikipedia.org/wiki/Aleph_(matem%C3%A1tica)
http://pt.wikipedia.org/wiki/Conjunto_cont%C3%A1vel
http://pt.wikipedia.org/wiki/Axioma_da_escolha
http://pt.wikipedia.org/wiki/Axiomas_de_Zermelo-Fraenkel

[Logica-l] E. W. Beth Dissertation Prize: 2012 new call for nominations

2012-05-14 Por tôpico Ruy de Queiroz
E. W. Beth Dissertation Prize: 2012 new call for nominations

Since 2002, FoLLI (the Association for Logic, Language, and
Information, http://www.folli.org) awards the E.W. Beth Dissertation
Prize to outstanding dissertations in the fields of Logic, Language,
and Information. We invite submissions for the best dissertation which
resulted in a Ph.D. degree in the year 2011. The dissertations will be
judged on technical depth and strength, originality, and impact made
in at least two of three fields of Logic, Language, and Computation.
Interdisciplinarity is an important feature of the theses competing
for the E.W. Beth Dissertation Prize.

Who qualifies.

Nominations of candidates are admitted who were awarded a Ph.D. degree
in the areas of Logic, Language, or Information between January 1st,
2011 and December 31st, 2011. There is no restriction on the
nationality of the candidate or the university where the Ph.D. was
granted. After a careful consideration, FoLLI has decided to accept
only dissertations written in English. Dissertations produced in 2011
but not written in English or not translated will be allowed for
submission, after translation, also with the call next year (for
dissertations defended in 2012). The present call for nominations for
the E.W. Beth Disertation Award 2012 will also accept nominations of
full English translations of theses originally written in another
language than English and defended in 2010 or 2011.

Prize.

The prize consists of:

-a certificate

-a donation of 2500 euros provided by the E.W. Beth Foundation

-an invitation to submit the thesis (or a revised version of it) to
the FoLLI Publications on Logic, Language and Information (Springer).
For further information on this series see the FoLLI site.

How to submit.

Only electronic submissions are accepted. The following documents are required:

1. The thesis in pdf or ps format (doc/rtf not accepted);

2. A ten page abstract of the dissertation in ascii or pdf format;

3. A letter of nomination from the thesis supervisor. Self-nominations
are not admitted: each nomination must be sponsored by the thesis
supervisor. The letter of nomination should concisely describe the
scope and significance of the dissertation and state when the degree
was officially awarded;

4. Two additional letters of support, including at least one letter
from a referee not affiliated with the academic institution that
awarded the Ph.D. degree.

All documents must be submitted electronically to bus...@amu.edu.pl.
Hard copy submissions are not admitted. In case of any problems with
the email submission or a lack of notification within three working
days, nominators should write to bus...@amu.edu.pl.

Important dates:

Deadline for Submissions: May 1, 2012. *Extended: June 30, 2012*.
Notification of Decision: July 31, 2012.

Explanation:

Due to some technical obstacles, the first call for nominations was
announced on the site of FoLLI in the beginning of March 2012 but not
widely distributed through mailing lists. Therefore we essentially
prolong the deadline now. We ask all potential nominators to inform
the chair earlier by a mail to bus...@amu.edu.pl, even before having
completed the required documents.

Committee :

Chris Barker (New York)

Wojciech Buszkowski (chair) (Poznan)

Dale Miller (Palaiseau)

Larry Moss (Bloomington)

Ian Pratt-Hartmann (Manchester)

Ruy de Queiroz (Recife)

Giovanni Sambin (Padua)

Rob van der Sandt (Nijmegen)

Rineke Verbrugge (Groningen)

Heinrich Wansing (Bochum)
___
Logica-l mailing list
Logica-l@dimap.ufrn.br
http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l


[Logica-l] LFCS 2013, San Diego, January 6-8: First Call for Papers

2012-03-29 Por tôpico Ruy de Queiroz
**
FIRST CALL FOR PAPERS
SYMPOSIUM ON LOGICAL FOUNDATIONS OF COMPUTER SCIENCE 2013 (LFCS'13) San
Diego, California, January 6-8, 2013

The LFCS series provides an outlet for the fast-growing body of work in the
logical foundations of computer science, e.g., areas of fundamental
theoretical logic related to computer science. The LFCS series began with
Logic at Botik, Pereslavl-Zalessky, 1989, and was co-organized by Albert R.
Meyer (MIT) and  Michael Taitslin (Tver), after which organization passed
to Anil Nerode.

LFCS Steering Committee: Anil Nerode - General Chair, Stephen Cook, Dirk
van Dalen, Yuri Matiyasevich, J. Alan Robinson, Gerald Sacks, Dana Scott.

LFCS Topics of interest include, but are not limited to: constructive
mathematics and type theory; logic, automata and automatic structures;
computability and randomness; logical foundations of programming; logical
aspects of computational complexity; logic programming and constraints;
automated deduction and interactive theorem proving; logical methods in
protocol and program verification; logical methods in program specification
and extraction; domain theory logic; logical foundations of database
theory;  equational logic and term rewriting; lambda and combinatory
calculi; categorical logic and topological semantics; linear logic;
epistemic and temporal logics;  intelligent and multiple agent system
logics; logics of proof and justification; nonmonotonic reasoning; logic in
game theory and social software; logic of hybrid systems; distributed
system logics; mathematical fuzzy logic; system design logics; other logics
in computer science.

LFCS'13 Program Committee: Sergei Artemov (New York) - PC Chair; Steve
Awodey (CMU); Alexandru Baltag (Oxford); Andreas Blass (Ann Arbor); Samuel
Buss (San Diego); Walter Dean (Warwick); Rod Downey (Wellington, NZ); Ruy
de Queiroz (Recife, Brazil); Antonio Montalban (Chicago); Rosalie Iemhoff
(Ultrecht); Bakhadyr Khoussainov (Auckland, NZ); Roman Kuznets (Bern);
Lawrence Moss (Bloomington, IN); Robert Lubarsky (Florida Atlantic
University); Victor Marek (Lexington, KY); Franco Montagna (Siena); Anil
Nerode (Cornell) - General LFCS Chair; Mati Pentus (Moscow); Jeffrey Remmel
(San Diego); Bryan Renne (Amsterdam); Philip Scott (Ottawa); Alex Simpson
(Edinburgh); Sonja Smets (Groningen); Michael Rathjen (Leeds); Alasdair
Urquhart (Toronto); Michael Zakharyashchev (London).

LFCS'13 Local Organizing Committee: Jeff Remmel (Chair), Samuel Buss,
Victor Marek.

Submission details. Proceedings will be published in the LNCS series.
There will be a post-conference volume of selected works published in the
Annals of Pure and Applied Logic. Submissions should be made electronically
via http://www.easychair.org/LFCS13/. Submitted papers must be in pdf/12pt
format and of no more than 15 pages, present work not previously published,
and must not be submitted concurrently to another conference with refereed
proceedings. LFCS has established the best student paper award and named it
after John Barkley Rosser Sr. (1907–1989), a prominent American logician
with fundamental contributions in both Mathematics and Computer Science.

Important Dates:
Submissions deadline (firm): September 10, 2012;
Notification: October 5, 2012;
Final papers for proceedings: October 15, 2012;
Symposium dates: January 6 - 8, 2013.
___
Logica-l mailing list
Logica-l@dimap.ufrn.br
http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l


[Logica-l] WoLLIC 2012 - Chamada de Trabalhos

2012-03-16 Por tôpico Ruy de Queiroz
://www.loria.fr/~areces/ (Cordoba)
   - Marcelo Arenas http://web.ing.puc.cl/~marenas/ (Santiago)
   - Steve Awodey http://www.andrew.cmu.edu/user/awodey/ (Pittsburgh)
   - Verónica Becher http://www-2.dc.uba.ar/profesores/becher/ (Buenos
   Aires)
   - Patrick Blackburn http://www.patrickblackburn.org/ (Roskilde)
   - Maribel Fernandez http://www.dcs.kcl.ac.uk/staff/maribel/ (London)
   - Santiago Figueira http://www.glyc.dc.uba.ar/santiago/ (Buenos Aires)
   - Marcelo Finger http://www.ime.usp.br/~mfinger (São Paulo)
   - Marcelo Fiore http://www.cl.cam.ac.uk/~mpf23/ (Cambridge)
   - Yuxi Fu http://basics.sjtu.edu.cn/~yuxi/ (Shanghai)
   - Rosalie Iemhoff http://www.phil.uu.nl/~iemhoff/ (Utrecht)
   - Neil Immerman http://www.cs.umass.edu/~immerman/ (Amherst)
   - Jean-Pierre Jouannaud http://www.lix.polytechnique.fr/~jouannaud/
(Paris)
   - Makoto Kanazawa http://research.nii.ac.jp/~kanazawa/ (Tokyo)
   - Delia Kesner http://www.pps.jussieu.fr/~kesner/ (Paris)
   - Dexter Kozen http://www.cs.cornell.edu/~kozen/ (Ithaca)
   - Martin Lange http://www.uni-kassel.de/~mlange/ (Kassel)
   - Benedikt Löwe http://www.math.uni-hamburg.de/home/loewe/ (Amsterdam)
   - Dag Normann http://folk.uio.no/dnormann/ (Oslo)
   - Luke Ong http://www.comlab.ox.ac.uk/luke.ong/ (Oxford) (CHAIR)
   - Erik Palmgren http://www2.math.uu.se/staff/pages/?uname=palmgren
(Uppsala)
   - Sylvain Salvati http://www.labri.fr/perso/salvati/ (Bordeaux)
   - Philippe Schnoebelen http://www.lsv.ens-cachan.fr/~phs/ (Cachan)
   - Fernando Souza http://www.dmat.ufpe.br/~fsouza/ (Recife)
   - Kazushige Terui http://www.kurims.kyoto-u.ac.jp/~terui/ (Kyoto)

**

*Steering Committee*

   - Samson Abramksy, Johan van Benthem, Anuj Dawar, Joe Halpern, Wilfrid
   Hodges, Daniel Leivant, Angus Macintyre, Grigori Mints, Hiroakira Ono, Ruy
   de Queiroz.

**

*Organising Committee*

   - Carlos Areces http://www.loria.fr/~areces/ (U Nacional Cordoba)
   (co-chair) (Local co-chair)
   - Santiago Figueira http://www.glyc.dc.uba.ar/santiago/ (U Buenos
   Aires) (Local co-chair)
   - Anjolina G. de Oliveira http://www.cin.ufpe.br/~ago (U Fed
   Pernambuco)
   - Ruy de Queiroz http://www.cin.ufpe.br/~ruy (U Fed Pernambuco)
   (co-chair)


*Further information*
Contact one of the Co-Chairs of the Organising Committee.

*Web page*
http://wollic.org/wollic2012/

*Last modified: March 16, 2012 07:52am GMT-3.*
___
Logica-l mailing list
Logica-l@dimap.ufrn.br
http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l


[Logica-l] E. W. Beth Dissertation Prize: 2012 call for nominations

2012-03-01 Por tôpico Ruy de Queiroz
*E. W. Beth Dissertation Prize: 2012 call for nominations*

Since 2002, FoLLI (the Association for Logic, Language, and
Information, http://www.folli.org) awards the E.W. Beth Dissertation
Prize to outstanding dissertations in the fields of Logic, Language,
and Information. We invite submissions for the best dissertation which
resulted in a Ph.D. degree in the year 2011. The dissertations will be
judged on technical depth and strength, originality, and impact made
in at least two of three fields of Logic, Language, and Computation.
Interdisciplinarity is an important feature of the theses competing
for the E.W. Beth Dissertation Prize.

Who qualifies.

Nominations of candidates are admitted who were awarded a Ph.D. degree
in the areas of Logic, Language, or Information between January 1st,
2011 and December 31st, 2011. There is no restriction on the
nationality of the candidate or the university where the Ph.D. was
granted. After a careful consideration, FoLLI has decided to accept
only dissertations written in English. Dissertations produced in 2011
but not written in English or not translated will be allowed for
submission, after translation, also with the call next year (for
2012). The present call for nominations for the E.W. Beth Disertation
Award 2012 will also accept nominations of full English translations
of theses originally written in another language than English and
defended in 2010 or 2011.

Prize.

The prize consists of:

-a certificate

-a donation of 2500 euros provided by the E.W. Beth Foundation

-an invitation to submit the thesis (or a revised version of it) to
the FoLLI Publications on Logic, Language and Information (Springer).
For further information on this series see the FoLLI site.

How to submit.

Only electronic submissions are accepted. The following documents are required:

1. The thesis in pdf or ps format (doc/rtf not accepted);

2. A ten page abstract of the dissertation in ascii or pdf format;

3. A letter of nomination from the thesis supervisor. Self-nominations
are not admitted: each nomination must be sponsored by the thesis
supervisor. The letter of nomination should concisely describe the
scope and significance of the dissertation and state when the degree
was officially awarded;

4. Two additional letters of support, including at least one letter
from a referee not affiliated with the academic institution that
awarded the Ph.D. degree.

All documents must be submitted electronically to bus...@amu.edu.pl.
Hard copy submissions are not admitted. In case of any problems with
the email submission or a lack of notification within three working
days, nominators should write to bus...@amu.edu.pl.

Important dates:

Deadline for Submissions: May 1, 2012.
Notification of Decision: July 8, 2012.

Committee :

Chris Barker (New York)

Wojciech Buszkowski (chair) (Poznan)

Dale Miller (Palaiseau)

Larry Moss (Bloomington)

Ian Pratt-Hartmann (Manchester)

Ruy de Queiroz (Recife)

Giovanni Sambin (Padua)

Rob van der Sandt (Nijmegen)

Rineke Verbrugge (Groningen)

Heinrich Wansing (Bochum)
___
Logica-l mailing list
Logica-l@dimap.ufrn.br
http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l


Re: [Logica-l] Curso de Verão (Depto de Matemática): Homotopy Type Theory, por Peter Lumsdaine

2012-02-25 Por tôpico Ruy de Queiroz
Aos interessados: uma parte do material do curso de Lumsdaine foi por ele
disponibilizado em:

http://www.mathstat.dal.ca/~p.l.lumsdaine/misc_files/2012-02-recife/

Ruy


Em 5 de janeiro de 2012 08:21, Ruy de Queiroz r...@cin.ufpe.br escreveu:

 A quem interessar possa

 As datas do curso de Peter Lumsdaine estão confirmadas para:

  13 a 17 de Fevereiro
 23 e 24 de Fevereiro


 Estarei dando umas aulas de introdução ao assunto na semana anterior:

 8 a 10 de Fevereiro


  As aulas deverão ocorrer no Departamento de Matemática da UFPE, e a sala
 ainda está para ser confirmada.

 Ruy


 -- Mensagem encaminhada --
 De: Ruy de Queiroz r...@cin.ufpe.br
 Data: 24 de novembro de 2011 22:58
 Assunto: Curso de Verão (Depto de Matemática): Homotopy Type Theory, por
 Peter Lumsdaine
 Para: staff st...@cin.ufpe.br, posgrad posg...@cin.ufpe.br, grad-l 
 gra...@cin.ufpe.br



 Como parte do Programa de Verão 
 2012http://www.ufpe.br/verao/index.php?option=com_contentview=articleid=315Itemid=243
  (Departamento
 de Matemática – UFPE, 05 de Janeiro a 24 de Fevereiro de 2012), está
 confirmado o mini-curso sobre teoria dos tipos da homotopia, que pode
 interessar tanto a matemáticos quanto a cientistas da computação que
 trabalham com teoria dos tipos, semântica de linguagens de programação,
 provadores automáticos de teorema, e/ou teoria das categorias.

 Detalhes sobre inscrição podem ser obtidos por meio de solicitação por
 e-mail a verao2012.d...@ufpe.br

 Ruy
 ---

 Title: *Homotopy Type Theory*
 Instructor: Peter Lumsdaine 
 http://mathstat.dal.ca/~p.l.lumsdaine/(Dalhousie University, Canada)
 15 Feb 2012 - 24 Feb 2012

 Abstract:

 These talks will provide an introduction to Homotopy Type Theory -- the 
 exploration
 of a fascinating and fruitful connection between logic and algebraic
 topology that has emerged over the last few years.

 Dependent Type Theory is a logical system expressive enough to give a 
 foundation
 for mathematics, but at the same time very well-suited to computer
 implementation.  In particular, if provides the basic language of many
 proof assistants and formalisation systems -- in particular, Coq.

 For the most part, its connection to more traditional set-theoretic 
 foundations
 is clear and well-understood, and moving between the two does not require
 too much change in technique.  An exception to this is its treatment of
 equality, which seems considerably more subtle than in classical
 foundations (for reasons originally motivated by philosophical and
 computational considerations).

 The key idea of Homotopy Type Theory is that this strangeness is resolved
 if one considers types as corresponding not to classical sets, but to
 classical *spaces* (among which sets can still be discerned as the
 discrete spaces).  The subtlety of equality can then be understood as
 coming from the behavious of *paths* within a space, and be tamed using
 the insights of modern algebraic topology.

 Practically, this opens up applications in both directions: tools and 
 intuitions
 for working in the type theory on the one hand; and on the other hand, a
 very direct approach to the formalisation of algebraic topology.  More
 philosophically, it gives a new and beautiful outlook on the universe of
 mathematics, with spaces investigated not indirectly as constructed
 models, but as fundamental objects of the language, as basic as sets are
 in the classical picture.

 Besides introducing the general setting, I will discuss Voevodsky's Univalence
 Axiom (a strengthening of standard universe axioms), the concept of
 h-level (homotopical dimension), and higher inductive types (a technique
 for presenting a wide class of spaces, including cell complexes, within
 the type theory).

 I'll use the Coq proof assistant for some exercises and examples.  I won't
 assume previous familiarity with it, but I recommend getting it and
 trying out the interface beforehand.  It's available from
 http://coq.inria.fr/, and there are several good introductions online; I
 recommend the first few exercises from
 http://www.cis.upenn.edu/~bcpierce/sf/toc.html.  Warning: Coq can be
 dangerously addictive!  (In the words of Andrew Appel: Coq is the world's
 best video game.)

 Much more reading (both light and heavy) on Homotopy Type Theory can be
 found at http://homotopytypetheory.org.




___
Logica-l mailing list
Logica-l@dimap.ufrn.br
http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l


Re: [Logica-l] Curso de Verão (Depto de Matemática): Homotopy Type Theory, por Peter Lumsdaine

2012-02-08 Por tôpico Ruy de Queiroz
A quem interessar possa

Confirmados dias, horários e local:

*Introdução à Teoria Intuicionística de Tipos* (Ruy)
4a.feira, 08/02, 15-17hs, Sala D-005 (CIn-UFPE)
5a.feira, 09/02, 13-15hs, Sala D-005 (CIn-UFPE)
6a.feira, 10/02, 13-15hs, Sala D-005 (CIn-UFPE)

*Homotopy Type Theory* (Peter Lumsdaine)
13 a 17/02, 13-15hs, Sala D-005 (CIn-UFPE)


Ruy

Em 5 de janeiro de 2012 08:21, Ruy de Queiroz r...@cin.ufpe.br escreveu:

 A quem interessar possa

 As datas do curso de Peter Lumsdaine estão confirmadas para:

  13 a 17 de Fevereiro
 23 e 24 de Fevereiro


 Estarei dando umas aulas de introdução ao assunto na semana anterior:

 8 a 10 de Fevereiro


  As aulas deverão ocorrer no Departamento de Matemática da UFPE, e a sala
 ainda está para ser confirmada.

 Ruy


 -- Mensagem encaminhada --
 De: Ruy de Queiroz r...@cin.ufpe.br
 Data: 24 de novembro de 2011 22:58
 Assunto: Curso de Verão (Depto de Matemática): Homotopy Type Theory, por
 Peter Lumsdaine
 Para: staff st...@cin.ufpe.br, posgrad posg...@cin.ufpe.br, grad-l 
 gra...@cin.ufpe.br



 Como parte do Programa de Verão 
 2012http://www.ufpe.br/verao/index.php?option=com_contentview=articleid=315Itemid=243
  (Departamento
 de Matemática – UFPE, 05 de Janeiro a 24 de Fevereiro de 2012), está
 confirmado o mini-curso sobre teoria dos tipos da homotopia, que pode
 interessar tanto a matemáticos quanto a cientistas da computação que
 trabalham com teoria dos tipos, semântica de linguagens de programação,
 provadores automáticos de teorema, e/ou teoria das categorias.

 Detalhes sobre inscrição podem ser obtidos por meio de solicitação por
 e-mail a verao2012.d...@ufpe.br

 Ruy
 ---

 Title: *Homotopy Type Theory*
 Instructor: Peter Lumsdaine 
 http://mathstat.dal.ca/~p.l.lumsdaine/(Dalhousie University, Canada)
 15 Feb 2012 - 24 Feb 2012

 Abstract:

 These talks will provide an introduction to Homotopy Type Theory -- the 
 exploration
 of a fascinating and fruitful connection between logic and algebraic
 topology that has emerged over the last few years.

 Dependent Type Theory is a logical system expressive enough to give a 
 foundation
 for mathematics, but at the same time very well-suited to computer
 implementation.  In particular, if provides the basic language of many
 proof assistants and formalisation systems -- in particular, Coq.

 For the most part, its connection to more traditional set-theoretic 
 foundations
 is clear and well-understood, and moving between the two does not require
 too much change in technique.  An exception to this is its treatment of
 equality, which seems considerably more subtle than in classical
 foundations (for reasons originally motivated by philosophical and
 computational considerations).

 The key idea of Homotopy Type Theory is that this strangeness is resolved
 if one considers types as corresponding not to classical sets, but to
 classical *spaces* (among which sets can still be discerned as the
 discrete spaces).  The subtlety of equality can then be understood as
 coming from the behavious of *paths* within a space, and be tamed using
 the insights of modern algebraic topology.

 Practically, this opens up applications in both directions: tools and 
 intuitions
 for working in the type theory on the one hand; and on the other hand, a
 very direct approach to the formalisation of algebraic topology.  More
 philosophically, it gives a new and beautiful outlook on the universe of
 mathematics, with spaces investigated not indirectly as constructed
 models, but as fundamental objects of the language, as basic as sets are
 in the classical picture.

 Besides introducing the general setting, I will discuss Voevodsky's Univalence
 Axiom (a strengthening of standard universe axioms), the concept of
 h-level (homotopical dimension), and higher inductive types (a technique
 for presenting a wide class of spaces, including cell complexes, within
 the type theory).

 I'll use the Coq proof assistant for some exercises and examples.  I won't
 assume previous familiarity with it, but I recommend getting it and
 trying out the interface beforehand.  It's available from
 http://coq.inria.fr/, and there are several good introductions online; I
 recommend the first few exercises from
 http://www.cis.upenn.edu/~bcpierce/sf/toc.html.  Warning: Coq can be
 dangerously addictive!  (In the words of Andrew Appel: Coq is the world's
 best video game.)

 Much more reading (both light and heavy) on Homotopy Type Theory can be
 found at http://homotopytypetheory.org.




___
Logica-l mailing list
Logica-l@dimap.ufrn.br
http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l


[Logica-l] Fwd: Curso de Verão (Depto de Matemática): Homotopy Type Theory, por Peter Lumsdaine

2012-01-18 Por tôpico Ruy de Queiroz
A quem interessar possa

As datas do curso de Peter Lumsdaine estão confirmadas para:

13 a 17 de Fevereiro
23 e 24 de Fevereiro


Estarei dando umas aulas de introdução ao assunto na semana anterior:

8 a 10 de Fevereiro


As aulas deverão ocorrer no Departamento de Matemática da UFPE, e a sala
ainda está para ser confirmada.

Ruy


-- Mensagem encaminhada --
De: Ruy de Queiroz r...@cin.ufpe.br
Data: 24 de novembro de 2011 22:58
Assunto: Curso de Verão (Depto de Matemática): Homotopy Type Theory, por
Peter Lumsdaine
Para: staff st...@cin.ufpe.br, posgrad posg...@cin.ufpe.br, grad-l 
gra...@cin.ufpe.br



Como parte do Programa de Verão
2012http://www.ufpe.br/verao/index.php?option=com_contentview=articleid=315Itemid=243
(Departamento
de Matemática – UFPE, 05 de Janeiro a 24 de Fevereiro de 2012), está
confirmado o mini-curso sobre teoria dos tipos da homotopia, que pode
interessar tanto a matemáticos quanto a cientistas da computação que
trabalham com teoria dos tipos, semântica de linguagens de programação,
provadores automáticos de teorema, e/ou teoria das categorias.

Detalhes sobre inscrição podem ser obtidos por meio de solicitação por
e-mail a verao2012.d...@ufpe.br

Ruy
---

Title: *Homotopy Type Theory*
Instructor: Peter Lumsdaine
http://mathstat.dal.ca/~p.l.lumsdaine/(Dalhousie University, Canada)
15 Feb 2012 - 24 Feb 2012

Abstract:

These talks will provide an introduction to Homotopy Type Theory --
the exploration
of a fascinating and fruitful connection between logic and algebraic
topology that has emerged over the last few years.

Dependent Type Theory is a logical system expressive enough to give a
foundation
for mathematics, but at the same time very well-suited to computer
implementation.  In particular, if provides the basic language of many
proof assistants and formalisation systems -- in particular, Coq.

For the most part, its connection to more traditional set-theoretic foundations
is clear and well-understood, and moving between the two does not require
too much change in technique.  An exception to this is its treatment of
equality, which seems considerably more subtle than in classical
foundations (for reasons originally motivated by philosophical and
computational considerations).

The key idea of Homotopy Type Theory is that this strangeness is resolved
if one considers types as corresponding not to classical sets, but to
classical *spaces* (among which sets can still be discerned as the discrete
spaces).  The subtlety of equality can then be understood as coming from
the behavious of *paths* within a space, and be tamed using the insights of
modern algebraic topology.

Practically, this opens up applications in both directions: tools and
intuitions
for working in the type theory on the one hand; and on the other hand, a
very direct approach to the formalisation of algebraic topology.  More
philosophically, it gives a new and beautiful outlook on the universe of
mathematics, with spaces investigated not indirectly as constructed models,
but as fundamental objects of the language, as basic as sets are in the
classical picture.

Besides introducing the general setting, I will discuss Voevodsky's Univalence
Axiom (a strengthening of standard universe axioms), the concept of h-level
(homotopical dimension), and higher inductive types (a technique for
presenting a wide class of spaces, including cell complexes, within the type
 theory).

I'll use the Coq proof assistant for some exercises and examples.  I won't
assume previous familiarity with it, but I recommend getting it and trying
out the interface beforehand.  It's available from http://coq.inria.fr/,
and there are several good introductions online; I recommend the first few
exercises from http://www.cis.upenn.edu/~bcpierce/sf/toc.html.  Warning:
Coq can be
dangerously addictive!  (In the words of Andrew Appel: Coq is the world's
best video game.)

Much more reading (both light and heavy) on Homotopy Type Theory can be
found at http://homotopytypetheory.org.
___
Logica-l mailing list
Logica-l@dimap.ufrn.br
http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l


Re: [Logica-l] provas x demonstrações, em Lógica

2011-11-14 Por tôpico Ruy de Queiroz
Caro João Marcos,

Louvo teu esforço (hercúleo, por sinal) em tentar estabelecer uma
terminologia para uma área que já tem uma (bem) estabelecida. Concordo com
Valéria: há um limite para a discussão sobre terminologia. Francamente, os
argumentos em favor de demonstração não me convencem.

Como já te disse em mensagem anterior, considero o termo prova mais
adequado. Soaria no mínimo estranho o uso de demonstração para traduzir
diversos termos já consolidados como: proof object (concordo com Elaine),
proof construction, proofs as programs, proof system, zero-knowledge
proof (e, nesse contexto, prover versus verifier), proof term, etc.

Um abraço,

Ruy

Em 10 de novembro de 2011 05:23, Valeria de Paiva valeria.depa...@gmail.com
 escreveu:

 oi Joao Marcos,
 eu sabia que essa ia dar panos pra manga

 Ok, vamos la:
 (0) Nao corro da raia e concordo plenamente que precisamos discutir
 assuntos como a terminologia da area em que trabalhamos, mas nao
 podemos exagerar, ne?

 (1)
 Sobre a curiosa observação de que não dá para proibir termos consagrados
 pelo uso...
 eu tb esclareço que nao disse isso. Disse que pra mim 'e o uso que
 determina a lingua e nao pronunciamentos, seja de quem for. (Ainda que
 eu concorde que 'e necessario batalhar contra usos que nos parecam
 pouco apropriados, no final das contas vence o que o povo resolver
 usar. Pra matematica e pra tudo mais na lingua. )

 (2)  o argumento da eufonia pra mim nao 'e tao importante.

 (3)
 Não sei de onde exatamente teria saído a tal distinção entre
 demonstration (que segundo vocês significaria demonstração com
 premissas) e proof (que significaria demonstração sem premissas).

 bom, pra mim saiu  do pai de todos,  Natural Deduction:  a proof
 theoretical study, Dag Prawitz, pagina 24, linha -3, na edicao da
 Dover. Exceto que , como a Andrea corrigiu 'e distinção entre
 deduction and proof.

 (4)
  no discreto ramo da lógica contemporânea conhecido como *Teoria
  das Demonstrações* (que os matemáticos praticantes em geral ignoram
  por completo, e da qual poucos sequer ouviram falar, e que certamente
  ainda conta com pouquíssimas publicações realmente representativas na
  nossa língua) precisamos de termos técnicos precisos e cuidadosamente
  projetados/escolhidos, pois as demonstrações, as proposições
  demonstráveis e a própria noção de demonstrabilidade são seus
  _objetos de estudo_!

 Sim, concordamos em genero, numero e grau (com pedidos de desculpas
 pela falta de um teclado competente que faca os acentos necessarios!)
 com:

 1. o fato de que poucos matematicos sequer ouviram falar da teoria em
 questao
 2.  que esta conta com pouquissimas publicações (cortar-e-colar
 funciona...) representativas na nossa lingua;
  e principalmente com
 3. precisamos de termos técnicos precisos e cuidadosamente
 projetados/escolhidos, pois as demonstrações, as proposições
 demonstráveis e a própria noção de demonstrabilidade são seus
 _objetos de estudo_!

 Sim! Exatamente. mas eu posso chamar as demonstracoes de provas e a
 Teoria das demonstrações de teoria da prova pois acho que Teoria
 da Prova e' um nome tao bom quanto o inicial.

 Nao me sinto agredida de forma alguma pela mensagem, mas tambem (dessa
 vez somente, normalmente voce me convence...) nao estou convencida de
 que a mudanca de terminologia e' necessaria nesse caso. Os argumentos
 apresentados nao foram suficientes. Tente de novo.

 Abracos (com)provaveis,
 Valeria



 2011/11/9 Joao Marcos botoc...@gmail.com:
  [Disclaimer:
  esta mensagem representa apenas a minha _opinião_ (e a outra opinião
  de que outra pessoa ela poderia representar?), que eu gostaria de
  defender sem que ninguém se sentisse agredido com isto.]
 
 
  PessoALL:
 
  Sei que a maior parte das pessoas não vai se dar ao trabalho de ler
  esta longa mensagem.  Mas ficam registrados os argumentos --- quem
  sabe ao menos encontrarão tolerantes e bem dispostos leitores futuros?
 
  Agradeço as respostas enviadas, na lista ou em privado.  Vou tentar
  não ficar me alongando sobre o assunto em inúmeras réplicas, até
  porque não sou tão presunçoso a ponto de imaginar que um quixote
  sozinho possa mudar a terminologia de uma área --- supondo que ela já
  esteja de fato bem estabelecida no Brasil, como alguns parecem
  acreditar.  Acresço portanto apenas algumas breves clarificações sobre
  o que eu disse anteriormente, e respondo alguns dos pontos principais
  levantados pelos colegas.
 
 
  (0) Não tenho dúvida de que é mais fácil não fazer nada, permanecer
  acomodado ou até mesmo fingir que nunca ouvi falar do assunto do que
  realmente rever sistematicamente, de caso pensado, algumas das nossas
  práticas linguísticas.  Se um caso de sucesso pode ser relatado,
  contudo, posso eu próprio dizer que há vários anos abandonei a palavra
  prova _em Lógica_, e hoje posso afirmar, com orgulho,que o vício
  está inteiramente superado!  (Como é que diz mesmo a irmandade do
  AA, neste tipo de situação?)  ;-)
 
  Quem trabalha 

Re: [Logica-l] provas x demonstrações, em Lógica

2011-11-13 Por tôpico Ruy de Queiroz
Acrescento um exemplo relevante: apesar do termo théorie de la
démonstration ser usado em francês, veja como se intitula o laboratório de
Jussieu que faz pesquisa em teoria da prova no que se relaciona com a
computação:

Laboratoire goog_52851488
Preuves, Programmes et Systèmes http://www.pps.jussieu.fr/
Ruy

Em 13 de novembro de 2011 07:50, Ruy de Queiroz r...@cin.ufpe.br escreveu:

 Caro João Marcos,

 Louvo teu esforço (hercúleo, por sinal) em tentar estabelecer uma
 terminologia para uma área que já tem uma (bem) estabelecida. Concordo com
 Valéria: há um limite para a discussão sobre terminologia. Francamente, os
 argumentos em favor de demonstração não me convencem.

 Como já te disse em mensagem anterior, considero o termo prova mais
 adequado. Soaria no mínimo estranho o uso de demonstração para traduzir
 diversos termos já consolidados como: proof object (concordo com Elaine),
 proof construction, proofs as programs, proof system, zero-knowledge
 proof (e, nesse contexto, prover versus verifier), proof term, etc.

 Um abraço,

 Ruy

 Em 10 de novembro de 2011 05:23, Valeria de Paiva 
 valeria.depa...@gmail.com escreveu:

 oi Joao Marcos,
 eu sabia que essa ia dar panos pra manga

 Ok, vamos la:
 (0) Nao corro da raia e concordo plenamente que precisamos discutir
 assuntos como a terminologia da area em que trabalhamos, mas nao
 podemos exagerar, ne?

 (1)
 Sobre a curiosa observação de que não dá para proibir termos
 consagrados pelo uso...
 eu tb esclareço que nao disse isso. Disse que pra mim 'e o uso que
 determina a lingua e nao pronunciamentos, seja de quem for. (Ainda que
 eu concorde que 'e necessario batalhar contra usos que nos parecam
 pouco apropriados, no final das contas vence o que o povo resolver
 usar. Pra matematica e pra tudo mais na lingua. )

 (2)  o argumento da eufonia pra mim nao 'e tao importante.

 (3)
 Não sei de onde exatamente teria saído a tal distinção entre
 demonstration (que segundo vocês significaria demonstração com
 premissas) e proof (que significaria demonstração sem premissas).

 bom, pra mim saiu  do pai de todos,  Natural Deduction:  a proof
 theoretical study, Dag Prawitz, pagina 24, linha -3, na edicao da
 Dover. Exceto que , como a Andrea corrigiu 'e distinção entre
 deduction and proof.

 (4)
  no discreto ramo da lógica contemporânea conhecido como *Teoria
  das Demonstrações* (que os matemáticos praticantes em geral ignoram
  por completo, e da qual poucos sequer ouviram falar, e que certamente
  ainda conta com pouquíssimas publicações realmente representativas na
  nossa língua) precisamos de termos técnicos precisos e cuidadosamente
  projetados/escolhidos, pois as demonstrações, as proposições
  demonstráveis e a própria noção de demonstrabilidade são seus
  _objetos de estudo_!

 Sim, concordamos em genero, numero e grau (com pedidos de desculpas
 pela falta de um teclado competente que faca os acentos necessarios!)
 com:

 1. o fato de que poucos matematicos sequer ouviram falar da teoria em
 questao
 2.  que esta conta com pouquissimas publicações (cortar-e-colar
 funciona...) representativas na nossa lingua;
  e principalmente com
 3. precisamos de termos técnicos precisos e cuidadosamente
 projetados/escolhidos, pois as demonstrações, as proposições
 demonstráveis e a própria noção de demonstrabilidade são seus
 _objetos de estudo_!

 Sim! Exatamente. mas eu posso chamar as demonstracoes de provas e a
 Teoria das demonstrações de teoria da prova pois acho que Teoria
 da Prova e' um nome tao bom quanto o inicial.

 Nao me sinto agredida de forma alguma pela mensagem, mas tambem (dessa
 vez somente, normalmente voce me convence...) nao estou convencida de
 que a mudanca de terminologia e' necessaria nesse caso. Os argumentos
 apresentados nao foram suficientes. Tente de novo.

 Abracos (com)provaveis,
 Valeria



 2011/11/9 Joao Marcos botoc...@gmail.com:
  [Disclaimer:
  esta mensagem representa apenas a minha _opinião_ (e a outra opinião
  de que outra pessoa ela poderia representar?), que eu gostaria de
  defender sem que ninguém se sentisse agredido com isto.]
 
 
  PessoALL:
 
  Sei que a maior parte das pessoas não vai se dar ao trabalho de ler
  esta longa mensagem.  Mas ficam registrados os argumentos --- quem
  sabe ao menos encontrarão tolerantes e bem dispostos leitores futuros?
 
  Agradeço as respostas enviadas, na lista ou em privado.  Vou tentar
  não ficar me alongando sobre o assunto em inúmeras réplicas, até
  porque não sou tão presunçoso a ponto de imaginar que um quixote
  sozinho possa mudar a terminologia de uma área --- supondo que ela já
  esteja de fato bem estabelecida no Brasil, como alguns parecem
  acreditar.  Acresço portanto apenas algumas breves clarificações sobre
  o que eu disse anteriormente, e respondo alguns dos pontos principais
  levantados pelos colegas.
 
 
  (0) Não tenho dúvida de que é mais fácil não fazer nada, permanecer
  acomodado ou até mesmo fingir que nunca ouvi falar do assunto do que

[Logica-l] Lançamento do livro The Functional Interpretation of Logical Deduction (World Scientific)

2011-11-11 Por tôpico Ruy de Queiroz
Caros(as),

Estão todos convidados a comparecer ao lançamento do nosso livro (em
parceria com Anjolina e Dov Gabbay):

The Functional Interpretation of Logical
Deductionhttp://www.worldscibooks.com/compsci/8215.html(World
Scientific, Oct 2011):


Onde: *SBS Livraria Internacional* (Av. Conselheiro Rosa e Silva 1519,
Recife, em frente à ABA-Aflitos)
Quando: 6a. Feira, 02/12/11, às 19hs.

*Todos são bem-vindos!*

RSVP para r...@cin.ufpe.br

Ruy
___
Logica-l mailing list
Logica-l@dimap.ufrn.br
http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l


[Logica-l] WoLLIC 2012 - Call for Papers

2011-10-22 Por tôpico Ruy de Queiroz
)
   Marcelo Finger http://www.ime.usp.br/~mfinger (São Paulo)
   Marcelo Fiore http://www.cl.cam.ac.uk/~mpf23/ (Cambridge)
   Yuxi Fu http://basics.sjtu.edu.cn/~yuxi/ (Shanghai)
   Rosalie Iemhoff http://www.phil.uu.nl/~iemhoff/ (Utrecht)
   Neil Immerman http://www.cs.umass.edu/~immerman/ (Amherst)
   Jean-Pierre Jouannaud http://www.lix.polytechnique.fr/~jouannaud/
(Paris)
   Makoto Kanazawa http://research.nii.ac.jp/~kanazawa/ (Tokyo)
   Delia Kesner http://www.pps.jussieu.fr/~kesner/ (Paris)
   Dexter Kozen http://www.cs.cornell.edu/~kozen/ (Ithaca)
   Martin Lange http://www.uni-kassel.de/~mlange/ (Kassel)
   Benedikt Löwe http://www.math.uni-hamburg.de/home/loewe/ (Amsterdam)
   Dag Normann http://folk.uio.no/dnormann/ (Oslo)
   Luke Ong http://www.comlab.ox.ac.uk/luke.ong/ (Oxford) (CHAIR)
   Erik Palmgren http://www2.math.uu.se/staff/pages/?uname=palmgren
(Uppsala)
   Sylvain Salvati http://www.labri.fr/perso/salvati/ (Bordeaux)
   Pierre Schnoebelen http://www.lsv.ens-cachan.fr/~phs/ (Cachan)
   Fernando Souza http://www.dmat.ufpe.br/~fsouza/ (Recife)
   Kazushige Terui http://www.kurims.kyoto-u.ac.jp/~terui/ (Kyoto)

*Steering Committee*

   Samson Abramksy, Johan van Benthem, Anuj Dawar, Joe Halpern, Wilfrid
   Hodges, Daniel Leivant, Angus Macintyre, Grigori Mints, Hiroakira Ono, Ruy
   de Queiroz.

*Organising Committee*

   Carlos Areces http://www.loria.fr/~areces/ (U Nacional Cordoba)
   (co-chair) (Local co-chair)
   Santiago Figueira http://www.glyc.dc.uba.ar/santiago/ (U Buenos Aires)
   (Local co-chair)
   Anjolina G. de Oliveira http://www.cin.ufpe.br/~ago (U Fed Pernambuco)
   Ruy de Queiroz http://www.cin.ufpe.br/~ruy (U Fed Pernambuco)
   (co-chair)

*Further information*
Contact one of the Co-Chairs of the Organising Committee.

*Web page*
http://wollic.org/wollic2012/
___
Logica-l mailing list
Logica-l@dimap.ufrn.br
http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l


Re: [Logica-l] Palestra de Voevodsky (ganhador da medalha Fields em 2002) sobre a possível inconsistência da aritmética

2011-10-17 Por tôpico Ruy de Queiroz
Steve Awodey também teve que cancelar sua vinda, mas recomendou seu ex-aluno
Peter Lumsdaine http://mathstat.dal.ca/~p.l.lumsdaine/, que confirmou a
participação no Programa de Verão 2012 da
Matemática/UFPEhttp://www.ufpe.br/verao/
.

As palestras de Lumsdaine deverão acontecer nos dias 15, 16, 17, 22, 23 e 24
de Fevereiro de 2012.

Título e resumo estão no final desta mensagem.

Todos são bem-vindos!

Abraço,

Ruy

Title: Homotopy Type Theory

Abstract:

These talks will provide an introduction to Homotopy Type Theory --
the exploration of a fascinating and fruitful connection between logic
and algebraic topology that has emerged over the last few years.

Dependent Type Theory is a logical system expressive enough to give
a foundation for mathematics, but at the same time very well-suited
to computer implementation.  In particular, if provides the basic language
of many proof assistants and formalisation systems -- in particular, Coq.

For the most part, its connection to more traditional
set-theoretic foundations is clear and well-understood, and moving between
the two does not require too much change in technique.  An exception to
this is its treatment of equality, which seems considerably more subtle than
in classical foundations (for reasons originally motivated by philosophical
and computational considerations).

The key idea of Homotopy Type Theory is that this strangeness is resolved if
one considers types as corresponding not to classical sets, but to classical
*spaces* (among which sets can still be discerned as the discrete spaces).
 The subtlety of equality can then be understood as coming from the
behavious of *paths* within a space, and be tamed using the insights of
modern algebraic topology.

Practically, this opens up applications in both directions: tools
and intuitions for working in the type theory on the one hand; and on
the other hand, a very direct approach to the formalisation of
algebraic topology.  More philosophically, it gives a new and beautiful
outlook
on the universe of mathematics, with spaces investigated not indirectly as
constructed models, but as fundamental objects of the language, as basic as
sets are in the classical picture.

Besides introducing the general setting, I will discuss
Voevodsky's Univalence Axiom (a strengthening of standard universe axioms),
the concept of h-level (homotopical dimension), and higher inductive
types (a technique for presenting a wide class of spaces, including cell
complexes, within the type theory).

I'll use the Coq proof assistant for some exercises and examples.  I won't
assume previous familiarity with it, but I recommend getting it and trying
out the interface beforehand.  It's available from http://coq.inria.fr/, and
there are several good introductions online; I recommend the first few
exercises from http://www.cis.upenn.edu/~bcpierce/sf/toc.html.  Warning: Coq
can be dangerously addictive!  (In the words of Andrew Appel: Coq is
the world's best video game.)

Much more reading (both light and heavy) on Homotopy Type Theory can be
found at http://homotopytypetheory.org.


Em 27 de setembro de 2011 20:23, Ruy de Queiroz r...@cin.ufpe.br escreveu:
 Reviravolta! Voevodsky cancelou a sua vinda.
 Porém já encontramos um substituto: Steve Awodey, parceiro de Voevodsky no
 projeto Homotopy Type Theory and Univalent Foundations, já aceitou o
 convite, faltando apenas confirmar as datas.
 Assim que tiver os detalhes, divulgo na lista.
 Ruy

 Em 25 de setembro de 2011 09:17, Ruy de Queiroz r...@cin.ufpe.br
escreveu:

 A quem interessar possa
 A vinda de Voevodsky para o Programa de Verão da Matemática (UFPE) está
 praticamente acertada. Muito provavelmente, o período será de 12 a 17 de
 Fevereiro de 2012.
 Ruy

 Em 28 de julho de 2011 10:08, Ruy de Queiroz r...@cin.ufpe.br escreveu:

 Car*s,
 A vinda de Voevodsky para dar um curso de Verão no Departamento de
 Matemática da UFPE está bem encaminada. Muito provavelmente, o curso
deverá
 ocorrer na segunda metade de Fevereiro de 2012.
 Aproveito para informar que, motivado pela palestra de Voevodsky no
 WoLLIC 2011, decidí expandir o artigo publiquei no número especial da
ENTCS
 com as contribuições do LSFA 2010, resultando num material que depositei
 no arxiv.org:

 Propositional equality, identity types, and direct computational paths
 http://arxiv.org/abs/1107.1901

 O artigo foi submetido à publicação.
 Comentários são muito bem-vindos.
 Abraço,
 Ruy
 Em 14 de junho de 2011 15:48, Ruy de Queiroz r...@cin.ufpe.br escreveu:

 João Marcos,

 Em 14 de junho de 2011 11:58, Joao Marcos botoc...@gmail.com
escreveu:

 Talvez alguém que tenha comparecido ao WoLLIC deste ano possa nos
 explicar um pouco mais sobre os tais Univalent Foundations of
 Mathematics?


http://www.math.ias.edu/~vladimir/Site3/Univalent_Foundations_files/2011_WoLLIC.pdf

 Estive lá, sim. Mas não há como ser mais preciso por e-mail do que o
 material que ele próprio disponibiliza.
 Como já foi dito por Valéria, o foco

Re: [Logica-l] Premiacao no Concurso de Teses e Dissertações 2011 da SBC

2011-08-08 Por tôpico Ruy de Queiroz
Parabéns, Renata e Márcio!

Em 8 de agosto de 2011 11:35, Renata Wassermann ren...@ime.usp.brescreveu:

 Obrigada a todos pelos parabéns.
 Estou muito orgulhosa pelo Márcio e por termos uma tese de lógica
 reconhecida
 como trabalho de computação!

Importante!

Abraço,
Ruy



 Abraços,

 Renata.

 2011/8/3 Walter Carnielli walter.carnie...@gmail.com

  Caros
 
  Márcio Moretto Ribeiro
  e Renata Wassermann
 
 
  parabéns ao  Márcio  pale premiacao (primeiro  lugar)  no Concurso de
  Teses e Dissertações  do XXXI Congresso da Sociedade Brasileira de
  Computação de 2011!
  pela sua  tese de doutorado  Revisão de Crenças em Lógicas de
  Descrição e em Outras Lógicas não Clássicas,  e parabéns  `a Renata
  pela orientacao!
 
  Sinto-me  horado em  ter participado da Banca de Defesa da tese e em
  ter sido co-responsável pela vinda do Márcio ao CLE como  pos-doc!
 
  Um abraco,
 
  Walter
 
 
 
 
  --
  
  Prof. Dr. Walter Carnielli
  Visiting  Scholar
  School of Historical and Philosophical Studies
  Room G06  Ground  Floor
  Old Quad Building
  The University of  Melbourne
  3010 VIC
  Melbourne, Australia
 
  Website: http://www.cle.unicamp.br/prof/carnielli
  ---
 



 --
 Renata Wassermann
 Associate Professor
 Computer Science Department
 University of São Paulo
 ___
 Logica-l mailing list
 Logica-l@dimap.ufrn.br
 http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l

___
Logica-l mailing list
Logica-l@dimap.ufrn.br
http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l


[Logica-l] Verbetes da Wikipédia em português produzidos no CIn-UFPE

2011-07-07 Por tôpico Ruy de Queiroz
A quem interessar possa, aqui vai uma relação de verbetes da Wikipédia em
português produzidos e/ou ampliados por nossos alunos aqui no Centro de
Informática da UFPE. Trata-se, em sua grande maioria, de trabalho de
tradução do verbete em inglês já existente para a língua portuguesa.

Ruy
---
*Teoria dos Conjuntos*:
http://pt.wikipedia.org/wiki/N%C3%BAmero_de_Hartogs
http://pt.wikipedia.org/wiki/Axioma_do_conjunto_vazio
http://pt.wikipedia.org/wiki/Diagrama_de_Hasse
http://pt.wikipedia.org/wiki/For%C3%A7amento
http://pt.wikipedia.org/wiki/Cardinalidade
http://pt.wikipedia.org/wiki/Teoria_dos_conjuntos

*Lógica*:
http://pt.wikipedia.org/wiki/L%C3%B3gica_de_primeira_ordem
http://pt.wikipedia.org/wiki/Subestrutura

*Teoria da Computação*:
http://pt.wikipedia.org/wiki/O_Teorema_de_Cook%E2%80%93Levin
http://pt.wikipedia.org/wiki/PSPACE
http://pt.wikipedia.org/wiki/Classes_de_Complexidade
http://pt.wikipedia.org/wiki/Problema_da_Correspond%C3%AAncia_de_Post
http://pt.wikipedia.org/wiki/Teorema_de_Savitch
http://pt.wikipedia.org/wiki/Decidibilidade

*Criptografia*:
http://pt.wikipedia.org/wiki/Ataque_de_temporiza%C3%A7%C3%A3o
http://pt.wikipedia.org/wiki/Autenticador_de_mensagem
http://pt.wikipedia.org/wiki/Fun%C3%A7%C3%A3o_de_m%C3%A3o_%C3%BAnica
http://pt.wikipedia.org/wiki/Fun%C3%A7%C3%A3o_Arapuca
http://pt.wikipedia.org/wiki/Logaritmo_discreto
http://pt.wikipedia.org/wiki/Pseudo-aleatoriedade
http://pt.wikipedia.org/wiki/Ataque_de_cifrotexto_escolhido
http://pt.wikipedia.org/wiki/Ataque_de_cifrotexto-escolhido_adaptativo
http://pt.wikipedia.org/wiki/Hist%C3%B3ria_da_criptografia
http://pt.wikipedia.org/wiki/Alice_e_Bob
http://pt.wikipedia.org/wiki/%C3%81rvores_de_Merkle
http://pt.wikipedia.org/wiki/Provas_de_conhecimento-zero
http://pt.wikipedia.org/wiki/Purotexto
___
Logica-l mailing list
Logica-l@dimap.ufrn.br
http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l


Re: [Logica-l] Palestra de Voevodsky (ganhador da medalha Fields em 2002) sobre a possível inconsistência da aritmética

2011-06-14 Por tôpico Ruy de Queiroz
João Marcos,

Em 14 de junho de 2011 11:58, Joao Marcos botoc...@gmail.com escreveu:

 Talvez alguém que tenha comparecido ao WoLLIC deste ano possa nos
 explicar um pouco mais sobre os tais Univalent Foundations of
 Mathematics?

 http://www.math.ias.edu/~vladimir/Site3/Univalent_Foundations_files/2011_WoLLIC.pdf

 Estive lá, sim. Mas não há como ser mais preciso por e-mail do que o
material que ele próprio disponibiliza.

Como já foi dito por Valéria, o foco não é no problema da possível
(in)consistência da aritmética, mas na busca por novos fundamentos da
matemática com base na teoria de tipos de Martin-Löf (alternativamente a
ZFC). Como especialista em teoria da homotopia, Voevodsky está procurando
encontrar paralelos entre as construções da teoria construtiva de tipos (em
particular, o cálculo de construções) e os tipos de homotopia. E até mesmo
implementar as construções no sistema Coq. Segundo ele mesmo diz na sua
motivação, o ponto de partida foi o modelo grupóide da teoria de tipos
intensional construído por Martin Hofmann e Thomas Streicher (The Groupoid
Model Refutes Uniqueness of Identity Proofs, LICS 1994).

Aqui na UFPE estamos (eu e Luciana Vale, aluna do doutorado da Matemática)
tentando fazer uma leitura desse modelo a partir da reformulação da
interpretação funcional da igualdade proposicional que começamos a elaborar
desde o 9th Amsterdam Coll (1994), e que mais recentemente foi apresentada
no LSFA 2010 (The Functional Interpretation of Direct Computations).

Propus à Matemática trazer Voevodsky para o próximo Programa de Verão. Caso
se confirme, divulgo na lista.

Abraço,

Ruy


JM

 2011/6/6 Valeria de Paiva valeria.depa...@gmail.com:
  Marcelo,
 
  eu nem assisti a palestra ainda, mas todas as discusses que li, dizem que
 o
  apelo 'e pra uma fundamentacao usando Martin-Loeuf's teoria de tipos.
 
  abs
  Valeria
 
  2011/6/6 Marcelo Finger mfin...@ime.usp.br
 
  Acho que é um apelo por uma fundamentação paraconsistente.
 
 
  2011/6/6 Joao Marcos botoc...@gmail.com
 
   What if current foundations of mathematics are inconsistent?
   - Institute for Advanced Study, Princeton
   http://video.ias.edu/voevodsky-80th
  
  
   Have fun,
   JM
   ___
   Logica-l mailing list
   Logica-l@dimap.ufrn.br
   http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l
  
 
 
 
  --
  Marcelo Finger
   Departamento de Ciencia da Computacao
   Instituto de Matematica e Estatistica
   Universidade de Sao Paulo
   Rua do Matao, 1010
   05508-090Sao Paulo, SP Brazil
   Tel: +55 11 3091-9688, 3091-6135, 3091-6134 (fax)
   http://www.ime.usp.br/~mfinger
  ___
  Logica-l mailing list
  Logica-l@dimap.ufrn.br
  http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l
 
 
 
  --
  Valeria de Paiva
  http://www.cs.bham.ac.uk/~vdp/
  http://valeriadepaiva.org/www/
 



 --
 http://sequiturquodlibet.googlepages.com/
 ___
 Logica-l mailing list
 Logica-l@dimap.ufrn.br
 http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l

___
Logica-l mailing list
Logica-l@dimap.ufrn.br
http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l


Re: [Logica-l] A mais curta demonstra??o de que P =/= NP

2011-06-05 Por tôpico Ruy de Queiroz
Caros Walter, Steffen, e demais colegas,

A incorporação da auto-referência numa teoria da verdade pode ser tratada de
forma bem interessante quando se utiliza os chamados conjuntos
não-bem-fundados, da teoria de Honsell  Forti, e, posteriormente, Aczel.

Um aluno meu de doutorado chamado Sérgio da Silva Aguiar, professor da
Universidade Estadual do Oeste da Bahia (em Vitória da Conquista)
desenvolveu uma teoria semântica baseada em fluxos (streams) e o
resultado ficou bem interessante. A tese, intitulada Uma Análise da
Auto-Referência baseada em Fluxos Semânticos, foi defendida em Março de
2008. Aqui vai o resumo da tese:

O objetivo principal desse trabalho é apresentar uma teoria de fluxos
(streams em inglês), que são pares ordenados possivelmente aninhados, capaz
de analisar sentenças (proposições) em geral, incluindo aquelas que
apresentam auto-referência. Desejamos que uma teoria geral, como a teoria
dos conjuntos, possa fundamentá-las. Entretanto, teorias clássicas de
conjuntos como a ZFC controlam auto-referência por meio de um axioma - O
Axioma da Fundação. Por esse motivo fundamentamos nossa semântica numa
teoria mais abrangente desenvolvida por Honsell e Forti (1983) e
aperfeiçoada por Peter Aczel (1988) - A Teoria dos Hiperconjuntos. Na
perspectiva dos hiperconjuntos, estruturas com auto-referência
(circularidade) são admitidas sem problemas. Como desejamos analisar
sentenças, isto é, interpretá-las num certo mundo e avaliá-las, uma das
principais preocupações são os critérios filosóficos do que entendemos como
verdade. Por isso, começamos em nosso primeiro capítulo, fazendo um apanhado
geral das teorias filosóficas da verdade. Afim de compararmos o poder de
interpretação de teorias clássicas com teorias mais modernas como a dos
hiperconjuntos, apresentamos, ainda que muitoresumidamente, os principais
aspectos da teoria dos conjuntos (ZFC) e em seguida falamos sobre
hiperconjuntos, bissimulação e fluxos, cuja compreensão é essencial para a
semântica da linguagem em nossa abordagem. Com essas noções em mãos,
entendemos que podemos analisar proposições tidas como paradoxais. O
principal representante dos paradoxos com auto-referência é o assim chamado
Paradoxo do Mentiroso: Esta sentença é falsa. Algumas linguagens foram
desenvolvidas objetivando dar uma semântica adequada ao paradoxo, mas cadas
uma delas apresentaram problemas e sofreram críticas por apresentarem pontos
fracos sob alguns aspectos tidos como essenciais. Então, apresentamos
algumas abordagens, concebidas para minimizar esses problemas: as abordagens
de Bertrand Russel, Tarski, Kripke, Barwise  Etchemendy e de A. N. Prior. A
nossa abordagem baseou-se principalmente numa afirmação de Prior que toda
sentença pode ser entendida como uma afirmação de verdade sobre ela mesma.
Entretanto, apresenta também aspectos semelhantes às linguagens
desenvolvidas por Tarski (metalinguagens), Kripke (apelo semântico) e
Barwise  Etchemendy (semântica situacional). Desenvolvemos uma linguagem
que pode acomodar sentenças em geral, inclusive as que apresentam
auto-referência. Alguns problemas apresentados em abordagens multivaloradas
foram resolvidos, pois o nosso sistema não apresenta mais do que dois
valores para avaliação. Problemas de linguagens puramente sintáticas também
foram sanados, pois a nossa estrutura não é baseada apenas em aspectos
sintáticos e possui ponto fixo. Com isso acreditamos que, sem perdermos
intuição, ganhamos poder de interpretação. Acreditamos também que uma prova
pode ser interpretada como sendo um fluxo semântico, pois é nada mais que
uma seqüência de proposições adequadamente encadeadas. Sendo assim, no
último capítulo falamos sobre provas diretas e provas por absurdo. Um
resultado interessante é que a interpretação de provas por absurdo dá origem
a um objeto potencialmente infinito bissimilar à sentença do Mentiroso.


Um abraço,

Ruy


Em 5 de junho de 2011 07:42, Walter Carnielli
walter.carnie...@gmail.comescreveu:

 Caros:

 o  Steffen Lewitzka tem razão, assim como   bem apontaram para o
 ponto a Andrea   Loparic, o Décio Krause e o Marcelo Finger.

 É claro (acho importante esclarecer isso aos estudantes que nos lêm
 nesta lista)  que nem a minha,  nem a do  Steffen, são
 demonstrações   de coisa nenhuma.   À  parte o ponto que levantei ,
 sobre a noção de prova não excluir universalidade(e  a este
 respeito as  provas  aí se parecem mais  com  o  Paradoxo de Curry)
  o ponto  central  desse tipo de argumento  são as sentenças
 auto-referentes em relação à  sua  própria verdade  (não apenas
 inocentemente  auto-referentes, como   meu nome  é  Fulano se  sou
 Fulano) .

 Uma  das tarefas  essenciais das  diversas teorias da verdade que
 temos à disposição  é dar  um tratamento adequado a este  tipo de
 sentença sem estragar  o resto.

  Um tratamento assim  aparece na, chamada teoria  da verdade de
 Kripke-Feferman, pela qual as  sentenças desse  tipo  não são nem V
 nem F (e nesse ponto é uma teoria  parcial da 

Re: [Logica-l] cinco velinhas

2011-03-25 Por tôpico Ruy de Queiroz
Parabéns João Marcos!

Abraço,

Ruy

Em 25 de março de 2011 17:09, Ana Teresa a...@lia.ufc.br escreveu:

 Oi João,

 faço minhas as palavras da Valéria e do Mário.
 Obrigada pelo seu empenho na criação e administração da lista.
 Todos aprendemos muito nesta convivência virtual.

 Bjs
 Ana



 On Fri, 25 Mar 2011, Valeria de Paiva wrote:

  Epa!
 eu nao recebi essa mensagm do moderador da lista.
 (Ainda bem que meu gmail gosta do Mario!...)

 PARABENS Joao Marcos!!!  um trabalho excelente de manter a lista e
 todo mundo informado da tanta coisa interessante no mundo da logica.

 Abracos
 Valeria

 2011/3/25 Mario Benevides ma...@cos.ufrj.br:

 João,

 Você também merece os parabéns por manter esta lista durante estes 5
 anos.

 Muito obrigado e um forte abraço,

 Mario

 Em 24 de março de 2011 20:42, O Administrador da LOGICA-L 
 logica-l-ow...@dimap.ufrn.br escreveu:

  A LOGICA-L se auto-congratula pelos seus cinco anos de vida!
 E que venham mais, e melhores!!

 Com os nossos agradecimentos aos atuais 375 membros da lista,
 O Administrador da LOGICA-L
 ___
 Logica-l mailing list
 Logica-l@dimap.ufrn.br
 http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l




 --
 Federal University of Rio de Janeiro
 www.cos.ufrj.br/~mario
 ___
 Logica-l mailing list
 Logica-l@dimap.ufrn.br
 http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l




 --
 Valeria de Paiva
 http://www.cs.bham.ac.uk/~vdp/
 http://valeriadepaiva.org/www/
 ___
 Logica-l mailing list
 Logica-l@dimap.ufrn.br
 http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l


 ___
 Logica-l mailing list
 Logica-l@dimap.ufrn.br
 http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l


___
Logica-l mailing list
Logica-l@dimap.ufrn.br
http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l


[Logica-l] WoLLIC 2011 Call for Short Presentations and Participation

2011-03-09 Por tôpico Ruy de Queiroz
*WoLLIC 2011*

*Call for Short Presentations and Participation*

*WoLLIC* http://wollic.org/* *is an annual international forum on
inter-disciplinary research involving formal logic, computing and
programming theory, and natural language and reasoning. Each meeting
includes invited talks and tutorials as well as contributed papers. The
eighteenth WoLLIC will be held at the University of Pennsylvania,
Philadelphia, USA, from May 18th to 20th, 2011.

*Invited Speakers*

*Rajeev Alur* http://www.cis.upenn.edu/~alur/ (Philadelphia)
*Rosalie Iemhoff* http://www.phil.uu.nl/~iemhoff/eigen.html (Utrecht)
*John Mitchell* http://theory.stanford.edu/people/jcm/ (Stanford)
*Vladimir Voevodsky* http://www.math.ias.edu/~vladimir/Site3/home.html
(Princeton)
*Yoad Winter* http://www.phil.uu.nl/~yoad/ (Utrecht)
*Michael Zakharyaschev* http://www.dcs.bbk.ac.uk/~michael/ (London)

*P**roceedings* of WoLLIC 2011, including both invited and contributed
papers, will be published in advance of the meeting as volume 6642 in
Springer's LNCS http://www.springer.com/lncs series. The list of
contributed papers can be found here:
http://wollic.org/wollic2011/programme.html

In addition, abstracts will appear in the Conference Report section of
the *Logic
Journal of the IGPL*, and selected contributions will be published as a
special post-conference WoLLIC 2011 issue of the *Journal of Computer and
System Sciences* http://www.elsevier.com/locate/jcss.

*Short presentations *

In addition to the regular papers, WoLLIC 2011 program will include a short
presentation session consisting of 20 minutes talks. These talks can report
on work in progress, etc.

The organizers of the short presentation session are Lev Beklemishev and
Andre Scedrov. Abstracts of 5 to 10 pages should be sent to the conference
address wollic2...@easychair.org by April 1, 2011. They will be subject to
light reviewing. Accepted presentations will be distributed as a conference
booklet. Authors will be notified by April 6.

*Registration*

Early registration deadline is April 8, late registration deadline is May 8,
see http://wollic.org/wollic2011/registration.html

*Programme Committee*

Sergei Artemov http://web.cs.gc.cuny.edu/~sartemov/ (New York)
Jeremy Avigad http://www.andrew.cmu.edu/user/avigad/ (Pittsburgh)
Arnold Beckman http://www.cs.swan.ac.uk/~csarnold/ (Swansea)
Lev Beklemishev http://www.mi.ras.ru/~bekl/ (Moscow) (CHAIR)
Alessandro Berarducci http://www.dm.unipi.it/~berardu/ (Pisa)
Sam Buss http://www.math.ucsd.edu/~sbuss/ (San Diego)
Achim Jung http://www.cs.bham.ac.uk/~axj/ (Birmingham)
Benedikt Löwe http://staff.science.uva.nl/~bloewe/ (Amsterdam)
Janos Makowsky http://www.cs.technion.ac.il/~janos/ (Haifa)
Michael Moortgat http://www.let.uu.nl/~ctl/docenten/moortgat.html
(Utrecht)
Vincent van Oostrom http://www.phil.uu.nl/~oostrom/ (Utrecht)
Prakash Panangaden http://www.cs.mcgill.ca/~prakash/ (Montréal)
Rohit Parikh http://www.sci.brooklyn.cuny.edu/cis/parikh/ (New York)
Ruy de Queiroz http://www.cin.ufpe.br/~ruy (Recife)
Alexander Shen http://www.poncelet.ru/pers/shen.htm (Marseilles and
Moscow)
Bas Spitters http://www.cs.ru.nl/~spitters/ (Nijmegen)
Helmut Veith http://www7.in.tum.de/~veith/ (Wien)
Yde Venema http://staff.science.uva.nl/~yde/ (Amsterdam)
Scott Weinstein http://www.cis.upenn.edu/~weinstei/ (Philadelphia)
Frank Wolter http://www.csc.liv.ac.uk/~frank/ (Liverpool)

*Steering Committee*

Samson Abramksy, Johan van Benthem, Anuj Dawar, Joe Halpern, Wilfrid Hodges,
Daniel Leivant, Angus Macintyre, Grigori Mints, Hiroakira Ono, Ruy de
Queiroz.

*Organising Committee*

Vivek Nigam http://www.math.upenn.edu/~vnigam/ (U Penn)
Anjolina G. de Oliveira http://www.cin.ufpe.br/~ago (U Fed Pernambuco)
Ruy de Queiroz http://www.cin.ufpe.br/~ruy (U Fed Pernambuco) (co-chair)
Andre Scedrov http://www.cis.upenn.edu/~scedrov/ (U Penn) (co-chair)

*Further information*
Contact one of the Co-Chairs of the Organising Committee.

*Web page* http://wollic.org/wollic2011/

*S**ponsors*

Association for Symbolic Logic http://www.aslonline.org/ (ASL), the Interest
Group in Pure and Applied Logics http://www.cin.ufpe.br/~igpl (IGPL), The
Association for Logic, Language and Information
http://www.folli.org/ (FoLLI),
the European Association for Theoretical Computer
Sciencehttp://www.eatcs.org/ (EATCS),
the European Association for Computer Science Logic
http://www.eacsl.org/ (EACSL),
the Sociedade Brasileira de Computação http://www.sbc.org.br/ (SBC), and
the Sociedade Brasileira de Lógica http://www.cle.unicamp.br/sbl/ (SBL).
___
Logica-l mailing list
Logica-l@dimap.ufrn.br
http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l


[Logica-l] WoLLIC 2011 - Data-limite adiada

2011-01-04 Por tôpico Ruy de Queiroz
 version deadline (firm)

*Programme Committee*

   Sergei Artemov http://web.cs.gc.cuny.edu/~sartemov/ (New York)
   Jeremy Avigad http://www.andrew.cmu.edu/user/avigad/ (Pittsburgh)
   Arnold Beckman http://www.cs.swan.ac.uk/~csarnold/ (Swansea)
   Lev Beklemishev http://www.mi.ras.ru/~bekl/ (Moscow) (CHAIR)
   Alessandro Berarducci http://www.dm.unipi.it/~berardu/ (Pisa)
   Andreas Blass http://www.math.lsa.umich.edu/~ablass/ (Ann Arbor) (tbc)
   Sam Buss http://www.math.ucsd.edu/~sbuss/ (San Diego)
   Achim Jung http://www.cs.bham.ac.uk/~axj/ (Birmingham)
   Benedikt Löwe http://staff.science.uva.nl/~bloewe/ (Amsterdam)
   Janos Makowsky http://www.cs.technion.ac.il/~janos/ (Haifa)
   Michael Moortgat http://www.let.uu.nl/~ctl/docenten/moortgat.html
(Utrecht)
   Vincent van Oostrom http://www.phil.uu.nl/~oostrom/ (Utrecht)
   Prakash Panangaden http://www.cs.mcgill.ca/~prakash/ (Montréal)
   Rohit Parikh http://www.sci.brooklyn.cuny.edu/cis/parikh/ (New York)
   Ruy de Queiroz http://www.cin.ufpe.br/~ruy (Recife)
   Alexander Shen http://www.poncelet.ru/pers/shen.htm (Marseilles and
   Moscow)
   Bas Spitters http://www.cs.ru.nl/~spitters/ (Nijmegen)
   Helmut Veith http://www7.in.tum.de/~veith/ (Wien)
   Yde Venema http://staff.science.uva.nl/~yde/ (Amsterdam)
   Scott Weinstein http://www.cis.upenn.edu/~weinstei/ (Philadelphia)
   Frank Wolter http://www.csc.liv.ac.uk/~frank/ (Liverpool)

*Steering Committee*

   Samson Abramksy, Johan van Benthem, Anuj Dawar, Joe Halpern, Wilfrid
   Hodges, Daniel Leivant, Angus Macintyre, Grigori Mints, Hiroakira Ono, Ruy
   de Queiroz.

*Organising Committee*

   Vivek Nigam http://www.math.upenn.edu/~vnigam/ (U Penn)
   Anjolina G. de Oliveira http://www.cin.ufpe.br/~ago (U Fed Pernambuco)
   Ruy de Queiroz http://www.cin.ufpe.br/~ruy (U Fed Pernambuco)
   (co-chair)
   Andre Scedrov http://www.cis.upenn.edu/~scedrov/ (U Penn) (co-chair)

*Further information*
Contact one of the Co-Chairs of the Organising Committee.

*Web page*
http://wollic.org/wollic2011/
___
Logica-l mailing list
Logica-l@dimap.ufrn.br
http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l


[Logica-l] WoLLIC está ranqueado como B pe lo Australian Research Council entre 1.953 conferências internacionais

2010-12-23 Por tôpico Ruy de Queiroz
Foi com satisfação que constatamos que o WoLLIC http://wollic.org/
(registrado
no DBLP como: http://www.informatik.uni-trier.de/~ley/db/conf/wollic/),
criado em 1994 aqui no então Departamento de Informática da UFPE, e com o
inestimável apoio de diversos colegas do cenário de Lógica no Brasil, é hoje
uma conferência internacional com ranking B (entre A, B, C, e not
ranked) segundo o Australian Research Council (em avaliação realizada em
Fev/2010), em meio a outras 1.952 conferências internacionais (aí incluídas
ACM's, IEEE's, etc.). Trata-se de um reconhecimento já consolidado do ponto
de vista dos veículos de publicação (anais no LNCS da Springer, números
especiais de revistas como Theoretical Computer Science, Information and
Computation, Journal of Computer and System Sciences, Annals of Pure and
Applied Logic, Fundamenta Informaticae, Logic Journal of the IGPL).

A partir da página http://www.arc.gov.au/era/era_journal_list.htm#2 é
possível obter um arquivo Excel com as 1.953 conferências internacionais
classificadas:

 *Ranked Conference List*

For some disciplines, ranked conferences will be used as an indicator.
The discipline
matrices http://www.arc.gov.au/era/key_docs10.htm detail which disciplines
will use ranked conferences.

Institutions are also required to submit information about conference
publications from non-listed conferences.  For more information, refer to
the *ERA 2010 Submission Guidelineshttp://www.arc.gov.au/era/key_docs10.htm
*.

The final Ranked Conference List for ERA 2010 is now available:


   - Ranked Conference List - Excel
Formathttp://www.arc.gov.au/xls/ERA2010_conference_list.xls
   (411kb)

 The Ranked Conference List includes:


   - Conference title and acronym (where relevant)
  - ERA ID – unique to each listed conference
  - Up to 3 FoRs assigned to each conference
  - A single quality rating for each listed conference of A, B, C or not
  ranked. Conferences that are not ranked are legitimate
conferences, but may
  not be of consistent quality, or may be too new to be assigned a quality
  tier.

 *Please note:*
 The A tier for conferences is equivalent to the A* and A tiers for ranked
journals.
___
Logica-l mailing list
Logica-l@dimap.ufrn.br
http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l


[Logica-l] WoLLIC 2011 - Chamada de Trabalhos - Prazo-limite se aproxima (01/Jan/2011)

2010-12-16 Por tôpico Ruy de Queiroz
/~sartemov/ (New York)
   Jeremy Avigad http://www.andrew.cmu.edu/user/avigad/ (Pittsburgh)
   Arnold Beckman http://www.cs.swan.ac.uk/~csarnold/ (Swansea)
   Lev Beklemishev http://www.mi.ras.ru/~bekl/ (Moscow) (CHAIR)
   Alessandro Berarducci http://www.dm.unipi.it/~berardu/ (Pisa)
   Andreas Blass http://www.math.lsa.umich.edu/~ablass/ (Ann Arbor) (tbc)
   Sam Buss http://www.math.ucsd.edu/~sbuss/ (San Diego)
   Achim Jung http://www.cs.bham.ac.uk/~axj/ (Birmingham)
   Benedikt Löwe http://staff.science.uva.nl/~bloewe/ (Amsterdam)
   Janos Makowsky http://www.cs.technion.ac.il/~janos/ (Haifa)
   Michael Moortgat http://www.let.uu.nl/~ctl/docenten/moortgat.html
(Utrecht)
   Vincent van Oostrom http://www.phil.uu.nl/~oostrom/ (Utrecht)
   Prakash Panangaden http://www.cs.mcgill.ca/~prakash/ (Montréal)
   Rohit Parikh http://www.sci.brooklyn.cuny.edu/cis/parikh/ (New York)
   Ruy de Queiroz http://www.cin.ufpe.br/~ruy (Recife)
   Alexander Shen http://www.poncelet.ru/pers/shen.htm (Marseilles and
   Moscow)
   Bas Spitters http://www.cs.ru.nl/~spitters/ (Nijmegen)
   Helmut Veith http://www7.in.tum.de/~veith/ (Wien)
   Yde Venema http://staff.science.uva.nl/~yde/ (Amsterdam)
   Scott Weinstein http://www.cis.upenn.edu/~weinstei/ (Philadelphia)
   Frank Wolter http://www.csc.liv.ac.uk/~frank/ (Liverpool)

*Steering Committee*

   Samson Abramksy, Johan van Benthem, Anuj Dawar, Joe Halpern, Wilfrid
   Hodges, Daniel Leivant, Angus Macintyre, Grigori Mints, Hiroakira Ono, Ruy
   de Queiroz.

*Organising Committee*

   Vivek Nigam http://www.math.upenn.edu/~vnigam/ (U Penn)
   Anjolina G. de Oliveira http://www.cin.ufpe.br/~ago (U Fed Pernambuco)
   Ruy de Queiroz http://www.cin.ufpe.br/~ruy (U Fed Pernambuco)
   (co-chair)
   Andre Scedrov http://www.cis.upenn.edu/~scedrov/ (U Penn) (co-chair)

*Further information*
Contact one of the Co-Chairs of the Organising Committee.

*Web page*
http://wollic.org/wollic2011/
___
Logica-l mailing list
Logica-l@dimap.ufrn.br
http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l


[Logica-l] WoLLIC 2011, Philadelphia, 18-21 Maio 2011 - Chamada de Trabalhos

2010-11-16 Por tôpico Ruy de Queiroz
) (tbc)
   Sam Buss http://www.math.ucsd.edu/~sbuss/ (San Diego)
   Achim Jung http://www.cs.bham.ac.uk/~axj/ (Birmingham)
   Benedikt Löwe http://staff.science.uva.nl/~bloewe/ (Amsterdam)
   Janos Makowsky http://www.cs.technion.ac.il/~janos/ (Haifa)
   Michael Moortgat http://www.let.uu.nl/~ctl/docenten/moortgat.html
(Utrecht)
   Vincent van Oostrom http://www.phil.uu.nl/~oostrom/ (Utrecht)
   Prakash Panangaden http://www.cs.mcgill.ca/~prakash/ (Montréal)
   Rohit Parikh http://www.sci.brooklyn.cuny.edu/cis/parikh/ (New York)
   Ruy de Queiroz http://www.cin.ufpe.br/~ruy (Recife)
   Alexander Shen http://www.poncelet.ru/pers/shen.htm (Marseilles and
   Moscow)
   Bas Spitters http://www.cs.ru.nl/~spitters/ (Nijmegen)
   Helmut Veith http://www7.in.tum.de/~veith/ (Wien)
   Yde Venema http://staff.science.uva.nl/~yde/ (Amsterdam)
   Scott Weinstein http://www.cis.upenn.edu/~weinstei/ (Philadelphia)
   Frank Wolter http://www.csc.liv.ac.uk/~frank/ (Liverpool)

*Steering Committee*

   Samson Abramksy, Johan van Benthem, Anuj Dawar, Joe Halpern, Wilfrid
   Hodges, Daniel Leivant, Angus Macintyre, Grigori Mints, Hiroakira Ono, Ruy
   de Queiroz.

*Organising Committee*

   Vivek Nigam http://www.math.upenn.edu/~vnigam/ (U Penn)
   Anjolina G. de Oliveira http://www.cin.ufpe.br/~ago (U Fed Pernambuco)
   Ruy de Queiroz http://www.cin.ufpe.br/~ruy (U Fed Pernambuco)
   (co-chair)
   Andre Scedrov http://www.cis.upenn.edu/~scedrov/ (U Penn) (co-chair)

*Further information*
Contact one of the Co-Chairs of the Organising Committee.

*Web page*
http://wollic.org/wollic2011/
___
Logica-l mailing list
Logica-l@dimap.ufrn.br
http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l


[Logica-l] Tecnologia da Informação, Crescim ento Exponencial e Singularidade

2010-06-18 Por tôpico Ruy de Queiroz
Pode interessar aos colegas da lista de Lógica:

-

Saiu publicado na última 3a.feira (15/06, 15:11hs) no portal *Investimentos
e Notícias* (São Paulo), assim como no *Blog de Jamildo* (*Jornal do
Commercio* Online, Recife):  Tecnologia da Informação, Crescimento
Exponencial e a
Singularidadehttp://www.investimentosenoticias.com.br/ultimas-noticias/artigos-especiais/tecnologia-da-informacao-crescimento-exponencial-e-a-singularidade.html
.

(Outros artigos em temas correlatos: no blog *Os Ventos da
Liberdadehttp://osventosdaliberdade.blogspot.com/
*.)

Ruy

 Tecnologia da Informação, Crescimento Exponencial e a
Singularidadehttp://www.investimentosenoticias.com.br/ultimas-noticias/artigos-especiais/tecnologia-da-informacao-crescimento-exponencial-e-a-singularidade.html
 TER, 15 DE JUNHO DE 2010 15:11
 [image: 
E-mail]http://www.investimentosenoticias.com.br/index.php?option=com_mailtotmpl=componentlink=aHR0cDovL3d3dy5pbnZlc3RpbWVudG9zZW5vdGljaWFzLmNvbS5ici91bHRpbWFzLW5vdGljaWFzL2FydGlnb3MtZXNwZWNpYWlzL3RlY25vbG9naWEtZGEtaW5mb3JtYWNhby1jcmVzY2ltZW50by1leHBvbmVuY2lhbC1lLWEtc2luZ3VsYXJpZGFkZS5odG1s[image:
Imprimir]http://www.investimentosenoticias.com.br/index.php?view=articlecatid=87%3Aartigos-especiaisid=163912852%3Atecnologia-da-informacao-crescimento-exponencial-e-a-singularidadetmpl=componentprint=1layout=defaultpage=option=com_contentItemid=286[image:
PDF]http://www.investimentosenoticias.com.br/ultimas-noticias/artigos-especiais/tecnologia-da-informacao-crescimento-exponencial-e-a-singularidade/pdf.html

É bem verdade que o ritmo alucinante de evolução tecnológica parece estar
restrito aos computadores e à eletrônica, mas uma devida reflexão revela um
padrão mais sutil e mais onipresente no mundo contemporâneo do que se
imagina. Conforme vem demonstrando já há algum tempo Ray Kurzweil ao longo
de sua premiada, ainda que não completamente incontroversa, carreira de
cientista e futurólogo, não apenas a computação, mas também as comunicações,
as tecnologias biológicas (tais como seqüenciamento de DNA), as tecnologias
médicas (tais como a varredura não-invasiva e o conhecimento do cérebro
humano), as técnicas de aproveitamento da energia solar com a ajuda da
nanotecnologia, tudo isso experimenta um crescimento exponencial. Em suma,
onde há tecnologia da informação, observa-se um crescimento um tanto
previsível: a duplicação da potência (preço versus desempenho, capacidade,
largura de banda) a cada ano. E esse crescimento exponencial é suave,
gradual, incremental, matematicamente idêntico em cada ponto, mas, em última
instância, profundamente transformador.

Como a duplicação não acontece indefinidamente, a tecnologia da informação
progride através de uma série de curvas de crescimento denominadas de
S-curvas, cada uma representando um paradigma diferente. (Uma S-curva, ou
curva sigmoidal, assim denominada em 1844 por Pierre François Verhulst que a
estudou em relação ao crescimento de populações, começa com um estágio de
crescimento aproximadamente exponencial, e, à medida que se aproxima da
saturação, o crescimento desacelera e acaba parando. É quando ocorre a
mudança de paradigma.) Exemplo célebre, a Lei de Moore (“a quantidade de
transistores em um chip duplica a cada 18 meses, enquanto que o preço cai
pela metade”), enunciada nos anos 1960’s, não é o primeiro paradigma a
trazer o crescimento exponencial para a computação, lembra Kurzweil. Nos
anos 1950’s eram as válvulas que decresciam de tamanho, até que chegou a um
limite, e aí deram lugar aos transistores, que, por sua vez, foram
substituídos pelos circuitos integrados. No próximo paradigma, ao que tudo
indica, será a vez dos circuitos moleculares auto-organizáveis
tridimensionais.

Em palestra proferida na sede da Google em 01/07/2009 sobre seu livro a ser
lançado “How the Mind Works and How to Build One”, Kurzweil chama à atenção
para o fato de que já no seu início o século XXI demonstra que será uma era
na qual a própria natureza do que significa ser humano será não somente
enriquecida mas também desafiada, na medida em que a espécie humana rompe os
grilhões de seu legado genético, e atinge níveis inconcebíveis de
inteligência, progresso material e longevidade. A taxa de mudança de
paradigmas está hoje dobrando a cada década, de modo que, nesse ritmo, o
século XXI deverá testemunhar 20.000 anos de progresso. O livro, segundo
Kurzweil, é essencialmente sobre a possibilidade de se fazer uma engenharia
reversa do cérebro, mas ele se refere à mente de modo a trazer à tona as
questões fundamentais sobre a consciência. “Um cérebro se torna uma mente à
medida em que ele se mistura com seu próprio corpo, e, na verdade, nosso
círculo de identidade vai além do nosso corpo”, acrescenta Kurzweil,
afirmando que embora haja interação com o ambiente, não há uma clara
distinção entre quem somos e o que não somos. O propósito da engenharia
reversa do cérebro humano seria entender os princípios básicos da
inteligência.

Em uma cartada ainda mais audaciosa, 

Re: [Logica-l] Regras para a igualdade em Deducao Natural

2010-06-18 Por tôpico Ruy de Queiroz
Caros Eliane, Eduardo, e demais colegas,

Uma teoria da prova para a igualdade pode ser formulada de forma mais
natural quando termos e símbolos de função são cidadãos de primeira
classe, o que não ocorre com a Dedução Natural de Prawitz, tampouco com o
Cálculo de Seqüentes de Gentzen. A interpretação funcional de Curry-Howard
(e suas extensões, como, por exemplo, a Dedução Natural Rotulada) se
apresenta como um arcabouço mais apropriado.

Temos trabalhado nisso há algum tempo, e no final desta mensagem incluo
algumas referências bibliográficas.

Um abraço,

Ruy


   1. de Queiroz, R.  de Oliveira, A.: 200?, `Natural Deduction for
   Equality: The Missing Entity'. In *Advances in Natural Deduction*, E. H.
   Haeusler, L. C. Pereira  V. de Paiva (eds.), Kluwer, to appear.
   2. de Queiroz, R.  Gabbay, D.: 1999, `Labelled Natural Deduction'.
In *Logic,
   Language and Reasoning. Essays in Honor of Dov
Gabbay*http://www.springer.com/dal/home/philosophy/logic?SGWID=1-40392-22-33743914-0,
   H.J. Ohlbach and U. Reyle (eds.), volume 5 of *Trends in
Logic*http://www.springer.com/dal/home/philosophy/logic?SGWID=1-40392-69-173624612-0
series,
   Kluwer Academic Publishers, Dordrecht, June 1999, pp. 173-250.
   3. de Oliveira, A.  de Queiroz, R.: 1999, `A Normalization Procedure for
   the Equational Fragment of Labelled Natural
Deductionhttp://www.oup.co.uk/igpl/Volume_07/Issue_02/#oliviera
   '. *Logic Journal of the Interest Group in Pure and Applied
Logics*http://www.oup.co.uk/igpl
   , *7*(2):173-215 http://www.oup.co.uk/igpl/Volume_07/Issue_02/, 1999,
   Oxford Univ. Press. Full version of a paper presented at *2nd
WoLLIC'95*http://wollic.org/wollic95/welcome.txt,
   Recife, Brazil, July 1995. Abstract appeared in*Journal of the Interest
   Group in Pure and Applied Logics* http://www.oup.co.uk/igpl
*4*(2):330-332,
   1996.
   4. de Queiroz, R.  Gabbay, D.: 1994, `Equality in Labelled Deductive
   Systems and the Functional Interpretation of Propositional Equality'. In
   *Proceedings of the Ninth Amsterdam Colloquium*, Paul Dekker  Martin
   Stokhof (eds.), ILLC/Department of Philosophy, University of Amsterdam,
   1994, pp. 547-565.


Em 18 de junho de 2010 04:54, Elaine Pimentel
elaine.pimen...@gmail.comescreveu:

 Oi, Eduardo,

 Eu nao sou expert em deducao natural, mas me parece que a prova e' essa:

 Pabb'|-Qabb'  b=b'
 -
 Pabb'|-Qabb |-Pabb  b=b'
 ----
 |-Pabb' = Qabb   |-Pabb'
 -
 |-Qabb

 Abraco,

 Elaine.

 2010/6/18 Eduardo Ochs eduardoo...@gmail.com:
  Oi pessoas,
 
  acabei de descobrir, pela n-ésima vez, que eu sei menos de Dedução
  Natural do que deveria... 8-\
 
  Eu imaginava que as regras para igualdade fossem:
 
   ---=I
   b=b
 
   b=b'  Pabb
   --=E
   Pabb'
 
  e a partir delas todas as outras propriedades naturais da igualdade
  pudessem ser obtidas como regras derivadas... eu consigo
  reflexividade, simetria, transitividade e um monte de outras, mas não
  estou conseguindo substituição (b':=b):
 
   [Pabb']
  :
Qabb'  Pabb
===subst
Qabb
 
  Alguém sabe como derivá-la?
 
  Pra piorar: descobri (mas tomara que eu esteja errado) que o Prawitz
  fala bem pouco sobre igualdade no Natural Deduction... Num artigo
  que eu estou tentando ler com todos os detalhes,
 
   http://www.math.mcgill.ca/rags/ZML/ZML.PDF
 
  as regras =I e =E aparecem, mas nem sei de onde é que o autor as
  tirou... Dicas?... 8-/
 
   Obrigado,
 Eduardo Ochs
 eduardoo...@gmail.com
 http://angg.twu.net/
  ___
  Logica-l mailing list
  Logica-l@dimap.ufrn.br
  http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l
 
 --
 Elaine.
 -
 Elaine Pimentel  - DMat/UFMG

 Address: Departamento de Matematica
 Universidade Federal de Minas Gerais
 Av Antonio Carlos, 6627 - C.P. 702
 Pampulha - CEP 30.161-970
 Belo Horizonte - Minas Gerais - Brazil
 Phone:   55 31 3409-5970/3409-5994
 Fax:   55 31 3409-5692
 http://www.mat.ufmg.br/~elaine
 -
 ___
 Logica-l mailing list
 Logica-l@dimap.ufrn.br
 http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l

___
Logica-l mailing list
Logica-l@dimap.ufrn.br
http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l


Re: [Logica-l] Quimeras lotéricas emaranhadas

2010-06-04 Por tôpico Ruy de Queiroz
Caro Walter,

Em 4 de junho de 2010 13:11, Walter Carnielli
walter.carnie...@gmail.comescreveu:


 A surpresa é que  para classes  'altas''  o não- determinismo não faz mais
 diferença: de fato, por um  famoso teorema   de W. Savitch de   1970,
  PSpace = NPSpace e  EXPSpace = NEXPSpace.


Tenho a impressão de que teorema de Savitch não está relacionado ao fato de
as classes PSPACE e NPSPACE serem altas, mas sim ao fato de que o espaço é
reutilizável, mas o tempo não o é.

Um abraço,

Ruy
___
Logica-l mailing list
Logica-l@dimap.ufrn.br
http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l


Re: [Logica-l] Quimeras lotéricas emaranhadas

2010-06-04 Por tôpico Ruy de Queiroz
Prezado Claus,

Em 4 de junho de 2010 22:02, Claus Akira Horodynski Matsushigue 
clau...@ime.usp.br escreveu:

 Sim caro Ruy,

 tem a ver com a reutilização do mesmo espaço, o que não é possível
 com o tempo.  Mas lembremos que também tem a ver com a altura
 (tamanho) da classe, visto que também não se sabe se L=?NL (sendo
 L a classe do espaço logarítmico).

 De fato, no nível sublinear ocorre essa dificuldade peculiar. Ainda assim,
algo relacionado à reutilização do espaço ocorre também nesse nivel:
NL=co-NL (teorema de Immerman), o que não sabemos se acontece com NP e
co-NP, por exemplo. Como diz Sipser, isso mostra que nossa intuição sobre
computação ainda tem muitas lacunas.

Um abraço,

Ruy

Abraços, Claus


 2010/6/4 Ruy de Queiroz r...@cin.ufpe.br:
  Caro Walter,
 
  Em 4 de junho de 2010 13:11, Walter Carnielli 
 walter.carnie...@gmail.com
  escreveu:
 
  A surpresa é que  para classes  'altas''  o não- determinismo não faz
 mais
  diferença: de fato, por um  famoso teorema   de W. Savitch de   1970,
   PSpace = NPSpace e  EXPSpace = NEXPSpace.
 
  Tenho a impressão de que teorema de Savitch não está relacionado ao fato
 de
  as classes PSPACE e NPSPACE serem altas, mas sim ao fato de que o espaço
 é
  reutilizável, mas o tempo não o é.
  Um abraço,
  Ruy
 
 
  ___
  Logica-l mailing list
  Logica-l@dimap.ufrn.br
  http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l
 
 
 ___
 Logica-l mailing list
 Logica-l@dimap.ufrn.br
 http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l

___
Logica-l mailing list
Logica-l@dimap.ufrn.br
http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l


[Logica-l] WoLLIC 2007 Special Issue of Information and Computation

2010-03-03 Por tôpico Ruy de Queiroz
[image: Go to ScienceDirect® Home] http://www.sciencedirect.com/science
  *Recommended Articles*   *Sent By:*Ruy de Queiroz
 I thought you would find this useful on ScienceDirect.
 1.*Inside Front Cover: Editorial
Boardhttp://www.sciencedirect.com/science?_ob=GatewayURL_method=citationSearch_uoikey=B6WGK-4YH4RC3-1_origin=SDEMFRHTML_version=1md5=acfebbb85e34c320cfde786b211c3f3d
*
*Information and Computation, Volume 208, Issue 5, May 2010, Page IFC*


 2.*Editorial Board
(continued)http://www.sciencedirect.com/science?_ob=GatewayURL_method=citationSearch_uoikey=B6WGK-4YH4RC3-2_origin=SDEMFRHTML_version=1md5=cb8d0045afe83fa4ec409eafd25195fe
*
*Information and Computation, Volume 208, Issue 5, May 2010, Page i*


 3.*Logic, language, information and
computationhttp://www.sciencedirect.com/science?_ob=GatewayURL_method=citationSearch_uoikey=B6WGK-4XX15RR-1_origin=SDEMFRHTML_version=1md5=f8ed964409c29bfb09187105ff3980e7
*
*Information and Computation, Volume 208, Issue 5, May 2010, Pages 395-396*
Ruy de Queiroz
   4.*Continuation semantics for the Lambek–Grishin
calculushttp://www.sciencedirect.com/science?_ob=GatewayURL_method=citationSearch_uoikey=B6WGK-4XVK3WR-4_origin=SDEMFRHTML_version=1md5=56605519a490590a8efef95caa23ead6
*
*Information and Computation, Volume 208, Issue 5, May 2010, Pages 397-416*
Raffaella Bernardi, Michael Moortgat
   5.*On quantifier-rank equivalence between linear
ordershttp://www.sciencedirect.com/science?_ob=GatewayURL_method=citationSearch_uoikey=B6WGK-4XVK3WR-1_origin=SDEMFRHTML_version=1md5=e010340b0c7ca246d459a89f59177fb0
*
*Information and Computation, Volume 208, Issue 5, May 2010, Pages 417-432*
Ryan Siders
   6.*Hybrid logical analyses of the ambient
calculushttp://www.sciencedirect.com/science?_ob=GatewayURL_method=citationSearch_uoikey=B6WGK-4XVK3WR-2_origin=SDEMFRHTML_version=1md5=4003d6679919ef6dabe07ffd11848dbf
*
*Information and Computation, Volume 208, Issue 5, May 2010, Pages 433-449*
Thomas Bolander, René Rydhof Hansen
   7.*Structured anaphora to quantifier
domainshttp://www.sciencedirect.com/science?_ob=GatewayURL_method=citationSearch_uoikey=B6WGK-4XVK3WR-3_origin=SDEMFRHTML_version=1md5=a7af1cfc28ed5f05925cfba44c6fb19d
*
*Information and Computation, Volume 208, Issue 5, May 2010, Pages 450-473*
Adrian Brasoveanu
   8.*Adjunct elimination in Context Logic for
treeshttp://www.sciencedirect.com/science?_ob=GatewayURL_method=citationSearch_uoikey=B6WGK-4XVRYMB-1_origin=SDEMFRHTML_version=1md5=dec9df8e6ea2b2bbf1ec2128d508a8fa
*
*Information and Computation, Volume 208, Issue 5, May 2010, Pages 474-499*
Cristiano Calcagno, Thomas Dinsdale-Young, Philippa Gardner
   9.*A new mapping between combinatorial proofs and sequent calculus proofs
read out from logical flow
graphshttp://www.sciencedirect.com/science?_ob=GatewayURL_method=citationSearch_uoikey=B6WGK-4XW00B2-2_origin=SDEMFRHTML_version=1md5=d4a761447eac7ae9b4c1c41245b9d989
*
*Information and Computation, Volume 208, Issue 5, May 2010, Pages 500-509*
Alessandra Carbone
   10.*A modular and parameterized presentation of pregroup
calculushttp://www.sciencedirect.com/science?_ob=GatewayURL_method=citationSearch_uoikey=B6WGK-4XW00B2-3_origin=SDEMFRHTML_version=1md5=f04c7ffa47e8f25d0c88d48451d5b938
*
*Information and Computation, Volume 208, Issue 5, May 2010, Pages 510-520*
Annie Foret
   11.*Numerical constraints on XML
datahttp://www.sciencedirect.com/science?_ob=GatewayURL_method=citationSearch_uoikey=B6WGK-4XW00B2-1_origin=SDEMFRHTML_version=1md5=fbded3f463bdd16995d3ae85b21da1e4
*
*Information and Computation, Volume 208, Issue 5, May 2010, Pages 521-544*
Sven Hartmann, Sebastian Link
   12.*Modules over monads and initial
semanticshttp://www.sciencedirect.com/science?_ob=GatewayURL_method=citationSearch_uoikey=B6WGK-4XWMNBJ-1_origin=SDEMFRHTML_version=1md5=813b4bac5e11bc6d58ca331cf6587246
*
*Information and Computation, Volume 208, Issue 5, May 2010, Pages 545-564*
André Hirschowitz, Marco Maggesi
   13.*Functional interpretations of linear and intuitionistic
logichttp://www.sciencedirect.com/science?_ob=GatewayURL_method=citationSearch_uoikey=B6WGK-4XWMNBJ-2_origin=SDEMFRHTML_version=1md5=a2c2237f1a45e9e241401be249ca07b4
*
*Information and Computation, Volume 208, Issue 5, May 2010, Pages 565-577*
Paulo Oliva
   14.*A coinductive calculus of binary
treeshttp://www.sciencedirect.com/science?_ob=GatewayURL_method=citationSearch_uoikey=B6WGK-4XWMNBJ-3_origin=SDEMFRHTML_version=1md5=99cec14af279ee8febd47dc0a5407a00
*
*Information and Computation, Volume 208, Issue 5, May 2010, Pages 578-593*
Alexandra Silva, Jan Rutten
   15.*A sketch of a dynamic epistemic
semiringhttp://www.sciencedirect.com/science?_ob=GatewayURL_method=citationSearch_uoikey=B6WGK-4XWMNBJ-4_origin=SDEMFRHTML_version=1md5=2410199694a41778e1c526ca85831b30
*
*Information and Computation, Volume 208, Issue 5, May 2010, Pages 594-604*
Kim Solin

   Access the ScienceDirect *Info site*
http://www.info.sciencedirect.com/if you have

[Logica-l] WoLLIC 2010 - CFP - Prazo-limite se aproximando (28 Fev)

2010-02-22 Por tôpico Ruy de Queiroz
April 27, 2010: Final version deadline (firm)

*Programme Committee*

   *Verónica Becher* http://www-2.dc.uba.ar/profesores/becher/ (Buenos
   Aires)
   *Raffaella Bernardi* http://www.inf.unibz.it/~bernardi/ (Bolzano)
   *Ricardo Bianconi* http://www.ime.usp.br/~bianconi/ (São Paulo)
   *Vasco Brattka* http://cca-net.de/vasco/ (Cape Town)
   *Balder ten Cate* http://staff.science.uva.nl/~bcate/ (ENS, Cachan)
   *Bob Coecke* http://www.comlab.ox.ac.uk/people/bob.coecke/ (Oxford)
   *Adriana Compagnoni* http://www.cs.stevens.edu/~abc/ (Stevens)
   *Marcelo Coniglio* http://www.cle.unicamp.br/prof/coniglio/ (Campinas)
   *Anuj Dawar* http://www.cl.cam.ac.uk/~ad260/ (Cambridge), chair
   *Valentin Goranko* http://www2.imm.dtu.dk/~vfgo/ (Copenhagen)
   *Masahito Hasegawa* http://www.kurims.kyoto-u.ac.jp/~hassei/ (Kyoto U,
   Japan)
   *Rosalie Iemhoff* http://www.phil.uu.nl/~iemhoff/eigen.html (Utrecht)
   *Makoto Kanazawa* http://research.nii.ac.jp/~kanazawa/ (National
   Institute of Informatics, Japan)
   *Giuseppe Longo* http://www.di.ens.fr/~longo/ (CNRS  ENS, Paris)
   *Mike Mislove* http://www.entcs.org/mislove.html (Tulane)
   *Michael Norrish* http://nicta.com.au/people/norrishm (NICTA,
   Canberra)
   *Bart Selman* http://www.cs.cornell.edu/selman/ (Cornell)
   *Scott Weinstein* http://www.cis.upenn.edu/~weinstei/ (Penn)

*Organising Committee*

   Mauricio Ayala-Rincon http://www.mat.unb.br/~ayala/ (U Brasília,
   Brazil) (co-chair)
   Flávio L. C.
Mourahttp://www.cic.unb.br:9080/sitecic/departamento/docentes/flavio
(U
   Brasília, Brazil)
   Claudia Nalonhttp://www.cic.unb.br:9080/sitecic/departamento/docentes/cn
(U
   Brasília, Brazil)
   Anjolina G. de Oliveira http://www.cin.ufpe.br/~ago (U Fed Pernambuco,
   Brazil)
   Ruy de Queiroz http://www.cin.ufpe.br/~ruy (U Fed Pernambuco, Brazil)
   (co-chair)

*Steering Committee*

*Samson Abramsky, Johan van Benthem, Joe Halpern, Wilfrid Hodges, Daniel
Leivant, Angus Macintyre, Grigori Mints, Hiroakira Ono, Ruy de Queiroz.*

*Further information*

*Contact one of the Co-Chairs of the Organising Committee.*

*Web page*

*http://wollic.org/wollic2010/ *

*
*
___
Logica-l mailing list
Logica-l@dimap.ufrn.br
http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l


[Logica-l] WoLLIC 2010 - Chamada de Trabalhos

2010-01-14 Por tôpico Ruy de Queiroz
 deadline (firm)
April 11, 2010: Author notification
April 27, 2010: Final version deadline (firm)

***Steering Committee*

*Samson Abramsky, Johan van Benthem, Joe Halpern, Wilfrid Hodges, Daniel
Leivant, Angus Macintyre, Grigori Mints, Hiroakira Ono, Ruy de Queiroz.*

***Programme Committee*

   *Verónica Becher* http://www-2.dc.uba.ar/profesores/becher/ (Buenos
   Aires)
   *Raffaella Bernardi* http://www.inf.unibz.it/~bernardi/ (Bolzano)
   *Ricardo Bianconi* http://www.ime.usp.br/~bianconi/ (São Paulo)
   *Vasco Brattka* http://cca-net.de/vasco/ (Cape Town)
   *Balder ten Cate* http://staff.science.uva.nl/~bcate/ (ENS, Cachan)
   *Bob Coecke* http://www.comlab.ox.ac.uk/people/bob.coecke/ (Oxford)
   *Adriana Compagnoni* http://www.cs.stevens.edu/~abc/ (Stevens)
   *Marcelo Coniglio* http://www.cle.unicamp.br/prof/coniglio/ (Campinas)
   *Anuj Dawar* http://www.cl.cam.ac.uk/~ad260/ (Cambridge), chair
   *Valentin Goranko* http://www2.imm.dtu.dk/~vfgo/ (Copenhagen)
   *Masahito Hasegawa* http://www.kurims.kyoto-u.ac.jp/~hassei/ (Kyoto U,
   Japan)
   *Rosalie Iemhoff* http://www.phil.uu.nl/~iemhoff/eigen.html (Utrecht)
   *Makoto Kanazawa* http://research.nii.ac.jp/~kanazawa/ (National
   Institute of Informatics, Japan)
   *Giuseppe Longo* http://www.di.ens.fr/~longo/ (CNRS  ENS, Paris)
   *Mike Mislove* http://www.entcs.org/mislove.html (Tulane)
   *Michael Norrish* http://nicta.com.au/people/norrishm (NICTA,
   Canberra)
   *Bart Selman* http://www.cs.cornell.edu/selman/ (Cornell)
   *Scott Weinstein* http://www.cis.upenn.edu/~weinstei/ (Penn)

*Organising Committee*

   Mauricio Ayala-Rincon http://www.mat.unb.br/~ayala/ (U Brasília,
   Brazil) (co-chair)
   Flávio L. C.
Mourahttp://www.cic.unb.br:9080/sitecic/departamento/docentes/flavio
(U
   Brasília, Brazil)
   Claudia Nalonhttp://www.cic.unb.br:9080/sitecic/departamento/docentes/cn
(U
   Brasília, Brazil)
   Anjolina G. de Oliveira http://www.cin.ufpe.br/~ago (U Fed Pernambuco,
   Brazil)
   Ruy de Queiroz http://www.cin.ufpe.br/~ruy (U Fed Pernambuco, Brazil)
   (co-chair)

*Further information*
Contact one of the Co-Chairs of the Organising Committee.

*Web page*
http://wollic.org/wollic2010/
___
Logica-l mailing list
Logica-l@dimap.ufrn.br
http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l


[Logica-l] Amir Pnueli, Pioneer of Temporal Logic, Dies at 68

2009-11-16 Por tôpico Ruy de Queiroz
Amir Pnueli, Pioneer of Temporal Logic, Dies at 68
By KENNETH 
CHANGhttp://topics.nytimes.com/top/reference/timestopics/people/c/kenneth_chang/index.html?inline=nyt-per
Published: November 14, 2009
Amir Pnueli, who turned a philosopher’s explorations of time, logic and free
will into a critical technique for verifying the reliability of computers,
died on Nov. 2 in Manhattan. He was 68. (*leia
maishttp://www.nytimes.com/2009/11/15/us/15pnueli.html?_r=1ref=technology
*)
___
Logica-l mailing list
Logica-l@dimap.ufrn.br
http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l


[Logica-l] Recommended articles on ScienceDirect

2009-09-04 Por tôpico Ruy de Queiroz



Recommended Articles



Sent By:
Ruy de Queiroz
I thought you would find this useful on ScienceDirect.

 1.Inside Front Cover: Editorial BoardInformation and Computation, Volume 207, Issue 10, October 2009, Page IFC
2.Editorial Board (continued)Information and Computation, Volume 207, Issue 10, October 2009, Page i
 3.Logic, Language, Information and ComputationInformation and Computation, Volume 207, Issue 10, October 2009, Pages 969-970Grigori Mints, Valria de Paiva, Ruy de Queiroz
4.Operational set theory and small large cardinalsInformation and Computation, Volume 207, Issue 10, October 2009, Pages 971-979Solomon Feferman
 5.Situations in LTL as stringsInformation and Computation, Volume 207, Issue 10, October 2009, Pages 980-999Tim Fernando
6.On graph reasoningInformation and Computation, Volume 207, Issue 10, October 2009, Pages 1000-1014Renata de Freitas, Paulo A.S. Veloso, Sheila R.M. Veloso, Petrucio Viana
 7.Propositional games with explicit strategiesInformation and Computation, Volume 207, Issue 10, October 2009, Pages 1015-1043Bryan Renne
8.Relating state-based and process-based concurrency through linear logic (full-version)Information and Computation, Volume 207, Issue 10, October 2009, Pages 1044-1077Iliano Cervesato, Andre Scedrov
 9.Some specially formulated axiomizations for I0 manage to evade the Herbrandized version of the Second Incompleteness TheoremInformation and Computation, Volume 207, Issue 10, October 2009, Pages 1078-1093Dan E. Willard



Access the ScienceDirect Info site if you have questions about this message or other features of this service.


 
This email has been sent to you by ScienceDirect, a division of Elsevier B.V., Radarweg 29, 1043 NX Amsterdam, The Netherlands, Tel.+31 20 485 3911.
ScienceDirect respects your privacy and does not disclose, rent or sell your personal information to any non-affiliated third parties without your consent, except as may be stated in the ScienceDirect online privacy policy.
By using email or alert services, you agree to comply with the ScienceDirect Terms and Conditions.
 2009 ScienceDirect. All rights reserved. Any unauthorized use, reproduction, or transfer of this message or its contents, in any medium, is strictly prohibited. ScienceDirect is a registered trademark of Elsevier B.V.

___
Logica-l mailing list
Logica-l@dimap.ufrn.br
http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l


[Logica-l] WoLLIC 2010 - Primeira Chamada de Trabalhos

2009-07-18 Por tôpico Ruy de Queiroz
) 
 *Vasco Brattka* http://cca-net.de/vasco/ (Cape Town) 
 *Balder ten Cate* http://staff.science.uva.nl/%7Ebcate/ (ENS,
 Cachan) 
 *Bob Coecke* http://www.comlab.ox.ac.uk/people/bob.coecke/ (Oxford) 
 *Adriana Compagnoni* http://www.cs.stevens.edu/%7Eabc/ (Stevens) 
 *Marcelo Coniglio*
 http://www.cle.unicamp.br/prof/coniglio/ (Campinas) 
 *Anuj Dawar* http://www.cl.cam.ac.uk/%7Ead260/ (Cambridge), chair 
 *Valentin Goranko* http://www2.imm.dtu.dk/%7Evfgo/ (Copenhagen) 
 *Masahito Hasegawa*
 http://www.kurims.kyoto-u.ac.jp/%7Ehassei/ (Kyoto U, Japan) 
 *Rosalie Iemhoff*
 http://www.phil.uu.nl/%7Eiemhoff/eigen.html (Utrecht) 
 *Makoto Kanazawa*

 http://research.nii.ac.jp/%7Ekanazawa/ (National Institute of
 Informatics, Japan) 
 *Giuseppe Longo* http://www.di.ens.fr/%7Elongo/ (CNRS  ENS, Paris) 
 *Mike Mislove* http://www.entcs.org/mislove.html (Tulane) 
 *Michael Norrish* http://nicta.com.au/people/norrishm (NICTA,
 Canberra) 
 *Bart Selman* http://www.cs.cornell.edu/selman/ (Cornell) 
 *Scott Weinstein* http://www.cis.upenn.edu/%7Eweinstei/ (Penn) 


*Organising Committee*

 Mauricio Ayala-Rincon http://www.mat.unb.br/%7Eayala/ (U
 Brasília, Brazil) (co-chair) 
 Flávio L. C. Moura

 http://www.cic.unb.br:9080/sitecic/departamento/docentes/flavio (U
 Brasília, Brazil) 
 Claudia Nalon

 http://www.cic.unb.br:9080/sitecic/departamento/docentes/cn (U
 Brasília, Brazil) 
 Anjolina G. de Oliveira http://www.cin.ufpe.br/%7Eago (U Fed
 Pernambuco, Brazil) 
 Ruy de Queiroz http://www.cin.ufpe.br/%7Eruy (U Fed Pernambuco,
 Brazil) (co-chair) 


*Further information*
Contact one of the Co-Chairs of the Organising Committee.

*Web page*
http://wollic.org/wollic2010/

___
Logica-l mailing list
Logica-l@dimap.ufrn.br
http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l


[Logica-l] WoLLIC 2009 - Chamada para Participaç ão

2009-04-15 Por tôpico Ruy de Queiroz

[favor divulgar]

Call for Participation

/*16th Workshop on Logic, Language, Information and Computation*/ 
(/*WoLLIC 2009*/)

Tokyo, Japan
June 21-24, 2009
(SPECIAL: There will be a screening of George Csicsery's N is a Number: 
A Portrait of Paul Erdos http://zalafilms.com/films/nisanumber.html, 
with kind permission of the film director)


WoLLIC http://wollic.org is an annual international forum on 
inter-disciplinary research involving formal logic, computing and 
programming theory, and natural language and reasoning.  Each meeting 
includes invited talks and tutorials as well as contributed papers.


WoLLIC 2009 http://research.nii.ac.jp/wollic2009/ will be held from 
June 21 through 24, 2009, in the National Center of Sciences 
http://www.nii.ac.jp/index.php?action=pages_view_mainpage_id=469lang=english, 
the building that houses the National Institute of Informatics 
http://www.nii.ac.jp/index.php?action=pages_view_mainpage_id=59lang=english 
in central Tokyo. It is jointly sponsored by the Association for 
Symbolic Logic (ASL), the Interest Group in Pure and Applied Logics 
(IGPL), the Association for Logic, Language and Information (FoLLI), the 
European Association for Theoretical Computer Science (EATCS), the 
Sociedade Brasileira de Computacao (SBC), and the Sociedade Brasileira 
de Logica (SBL).


The proceedings of WoLLIC 2009 will appear as Volume 5514 of the 
FoLLI/LNAI 
http://www.springer.com/computer/lncs?SGWID=0-164-6-144181-0 subline 
of the Springer Lecture Notes in Computer Science 
http://www.springer.com/lncs.


*Special Event*
2009 will mark the 60-th anniversary of the publication of Paul Erdos' 
elementary proof of the Prime Number Theorem. WoLLIC will celebrate this 
by screening the documentary about Paul Erdos which was directed by 
George Csicsery N is a number - A Portrait of Paul Erdos 
http://zalafilms.com/films/nisanumber.html.

http://zalafilms.com/films/nisanumber.html
*Tutorial Lectures
*Arnold Beckmann (Swansea University): /Definable Search Problems in 
Bounded Arithmetic/*

*Thomas Eiter (Vienna University of Technology): /Reasoning Using Knots/*
*Frank Wolter (University of Liverpool): /From Mathematical Logic to 
Life Science Ontologies/*


Invited Talks
*Arnold Beckmann (Swansea University): /New Characterisations of 
Definable Search Problems/*
*Carlos Caleiro (Technical University of Lisbon): /Algebraic Valuations 
as Behavioral Logical Matrices/*
*Thomas Eiter (Vienna University of Technology): /Knot-Based Query 
Answering in Description Logic/*
*Sylvain Salvati (INRIA Bordeaux - Sud Ouest/LaBRI): /Recognizability in 
the Simply Typed Lambda-Calculus/*
*Taisuke Sato (Tokyo Institute of Technology): /Logic-Based 
Probabilistic Modeling/*
*Frank Wolter (University of Liverpool): /From Mathematical Logic to 
Life Science Ontologies/*


Contributed Papers
*Sebastian Link: Spoilt for Choice: /Full First-Order Hierarchical 
Decompositions/*

*Hubie Chen and Omer Gimenez: /On-the-fly Macros/*
*Juha Kontinen and Ville Nurmi: /Team Logic and Second-Order Logic/*
*Juliana Kaizer Vizzotto, André Rauber Du Bois and Amr Sabry: /The Arrow 
Calculus as a Quantum Programming Language/*
*Sara Miner More and Pavel Naumov: /An Independence Relation for Sets of 
Secrets/*
*Hugo Herbelin and Gyesik Lee: /Forcing-based cut-elimination for 
Gentzen-style intuitionistic sequent calculus/*
*Alexandru Baltag and Sonja Smets: /Learning by Questions and Answers: 
From Belief-Revision Cycles to Doxastic Fixed Points/*
*Matthias Baaz, Agata Ciabattoni and Norbert Preining: /SAT in Monadic 
Gödel Logics: a borderline between decidability and undecidability/*
*Philippe de Groote, Sylvain Pogodalla and Carl Pollard: /On the 
Syntax-Semantics Interface: from Convergent Grammar to Abstract 
Categorial Grammar/*
*Alain Lecomte and Myriam Quatrini: /Ludics and its Applications to 
Natural Language Semantics/*

*Bernhard Heinemann: /Observational Effort and Formally Open Mappings/*
*Bauer Kerstin, Raffaella Gentilini and Klaus Schneider: /Property 
Driven Three Valued Model Checking on Hybrid Automata/*
*Gleifer Alves, Anjolina Grisi de Oliveira and Ruy de Queiroz: 
/Transformations via geometric perspective techniques augmented with 
cycles normalization/*

*Linda Postniece: /Deep inference in bi-intuitionistic logic/*
*Katsuhiko Sano: /Sound and Complete Tree-Sequent Calculus for 
Inquisitive Logic/*

*Yoshihiro Maruyama: /A Duality for algebras of Lattice-Valued Modal Logic/*
*Joao Marcos and Carlos Caleiro: /Classic-like analytic tableaux for 
finite-valued logics/*

*Benjamin Rossman: /Ehrenfeucht-Fraisse Games on Random Structures/*
*Majid Alizadeh: /Completions of basic algebras/*
*Francesco Belardinelli and Alessio Lomuscio: /First-Order Linear-time 
Epistemic Logic with Group Knowledge: An Axiomatisation of the Monodic 
Fragment/
Cristian Prisacariu and Gerardo Schneider: /CL: An Action-based Logic 
for Reasoning about Contracts/*/

/*Ren-June Wang: /Knowledge, Time, and Logical