Oi Valéria, Acrescentar nominais e @ normalmente não muda a complexidade de problemas de validade, satisfabilidade e verificação de modelos. Isto é bem interessante do ponto de vista computacional.
Um abraço, Mario Em 23 de maio de 2012 09:09, Valeria de Paiva <valeria.depa...@gmail.com>escreveu: > nao entendi Mario...tem alguma definicao formal de hibridizacao ou e' so' > a ideia intuitiva de pegar uma logica modal e adicionar nominais da menor > maneira possivel? > > Valeria > > 2012/5/22 Mario Benevides <ma...@cos.ufrj.br> > >> Caros, >> >> Um outro aspecto muito interessante é que, *normalmente*, a >> "hibridização" (não estou falando de binders) de uma lógica modal não >> aumenta a complexidade de lógica modal por baixo. >> >> Um abraço, >> >> Mario >> >> Em 22 de maio de 2012 11:21, Valeria de Paiva >> <valeria.depa...@gmail.com>escreveu: >> >> oi Elaine, >>> A Sara tem sim, mas me parece que 'e o mesmo truque/insight do >>> Vigano/Simpson, so' que em forma de sequentes em vez de deducao natural, >>> o >>> que voce gosta mais...! >>> as limitacoes dos metodos tb sao semelhantes, teorias geometricas. >>> >>> all good stuff, como se diz por ai. >>> abs >>> valeria >>> >>> 2012/5/22 Elaine Pimentel <elaine.pimen...@gmail.com> >>> >>> > Olas! >>> > >>> > Eu nao vou ter tempo agora de escrever muito, mas acho que vale a pena >>> > dizer que me parece que a Sara Negri tem um "procedure" para gerar >>> > sistemas baseados em cálculo de sequentes para lógicas modais. >>> > >>> > Abraco, >>> > >>> > Elaine. >>> > >>> > 2012/5/21 Valeria de Paiva <valeria.depa...@gmail.com>: >>> > > oi Joao Marcos, >>> > > com certeza, o estilo de deducao natural do Basin, Vigano e Matthews, >>> > que o >>> > > Luca explicou muito melhor no livro e' uma outra maneira de >>> consertar os >>> > > formalismos dedutivos modais, da mesma forma que os sistemas do >>> Simpson >>> > tb >>> > > o sao, pra logica modal intuicionista. >>> > > as logicas hibridas levam essa ideia ao seu desenvolvimento natural. >>> > > se voce vai etiquetar as formulas pra dizer onde elas sao validas, >>> em vez >>> > > de colocar no sistema dedutivo simplesmente a relacao de >>> acessibilidade >>> > do >>> > > modelo, pode colocar os mundos tambem e usa-los nas formulas como >>> > cidadaos >>> > > de primeira classe. >>> > > e isso te da', como bem disse o Mario, muito mais expressividade no >>> > > sistema. >>> > > a minha resposta pro Tony nao 'e discordando da do Mario, mas sim >>> > > explicando o que *eu* vejo de interessante... >>> > > >>> > > Como a gente ja conversou muitas vezes, eu tenho varios "problemas >>> > > emocionais" com todos os formalismos que fazem essa coisa de fazer a >>> > > semantica parte da sintaxe, pois eu acho que isso 'e meio >>> > > "cheating",filosoficamente. tb 'e dar uma primazia especial aas >>> > semanticas >>> > > de mundos possiveis que eu nao sei se elas teem), mas a gente quer >>> usar >>> > > sistemas modais, a gente quer fazer contas/descobrir provas neles, e >>> isso >>> > > certamente 'e uma solucao implementavel... >>> > > >>> > > vamos conversando e melhorando o nosso entendimento dos nossos >>> sistemas, >>> > ne? >>> > > abs >>> > > Valeria >>> > > >>> > > On Mon, May 21, 2012 at 2:49 PM, Joao Marcos <botoc...@gmail.com> >>> wrote: >>> > > >>> > >> Olá, Valeria: >>> > >> >>> > >> Acho que vale a pena recordar ainda que há uma outra maneira >>> bastante >>> > >> simples de "consertar" os formalismos dedutivos modais, pelo >>> acréscimo >>> > >> de etiquetas (representando termos de uma assinatura de primeira >>> ordem >>> > >> adequada) sobre fórmulas modais e a adição de fórmulas relacionais à >>> > >> linguagem-objeto. Como resultado, regras de dedução natural >>> > >> extremamente simples para os principais sistemas modais podem ser >>> > >> definidas, tal como ilustradas no livro "Labelled Non-Classical >>> > >> Logics", de Luca Viganò --- ou no seguinte material nosso, em >>> > >> português: >>> > >> http://www.dimap.ufrn.br/~jmarcos/courses/LC/Cap4.pdf >>> > >> >>> > >> As lógicas híbridas, claro, vão muito além disso, sendo baseadas em >>> > >> linguagens legitimamente *mais expressivas* do ponto de vista das >>> > >> estruturas relacionais por elas caracterizadas, como Mário bem >>> chamou >>> > >> a atenção em sua mensagem. >>> > >> >>> > >> Abraços, >>> > >> Joao Marcos >>> > >> >>> > >> >>> > >> On Sat, May 19, 2012 at 1:01 PM, Valeria de Paiva >>> > >> <valeria.depa...@gmail.com> wrote: >>> > >> > Tony, >>> > >> > as far as I'm concerned the real advantage of hybrid logics over >>> > >> multimodal >>> > >> > logics is on their proof theoretical aspects, hybrid logics are >>> much >>> > >> better >>> > >> > behaved than modal logics as far as their proof theory goes. >>> Patrick >>> > >> > Blackburn gave a course in nasslli2002 where he pressed this >>> point and >>> > >> i've >>> > >> > spent an enjoyable half an hour trying to find the slides to send >>> you, >>> > >> but >>> > >> > have not. the reader for the course is available >>> > >> > www.stanford.edu/group/nasslli/courses/*blackburn*/reader.pdf. >>> > >> > >>> > >> > in particular interpolation results are recovered: >>> > >> > (Repairing the Interpolation Theorem in Quantified Modal >>> > >> > Logic<http://www.loria.fr/%7Eblackbur/papers/repairing.pdf>, >>> > >> > by Carlos Areces, Patrick Blackburn and Maarten Marx. *Annals of >>> Pure >>> > and >>> > >> > Applied Logic*, 124, 287-299, 2003. ) >>> > >> > >>> > >> > but for me the big payoff was on cut-elimination results for >>> several >>> > >> > systems. >>> > >> > >>> > >> > Patrick's lectures were impressive enough to make me investigate >>> > >> > constructive versions of hybrid logics with Torben Brauner to >>> begin >>> > with >>> > >> > and more recently with Herman Hauesler and Alexandre Rademaker. >>> > >> > >>> > >> > and yes, satisfaction operators do behave like modal operators. >>> > >> > >>> > >> > but no, it's not simply giving new names to old things, since >>> using >>> > the >>> > >> > satisfaction operators and internalizing the models as part of >>> your >>> > >> syntax >>> > >> > you genuinely get a different logic system, which has different >>> > >> inferential >>> > >> > properties and which you can implement and do more things with. >>> > >> > at least this is my take. >>> > >> > >>> > >> > []s, >>> > >> > Valeria >>> > >> >>> > >> -- >>> > >> http://sequiturquodlibet.googlepages.com/ >>> > >> >>> > > >>> > > >>> > > >>> > > -- >>> > > 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 >>> > >>> > >>> > >>> > -- >>> > Elaine. >>> > -------------------------------------------------------- >>> > Elaine Pimentel >>> > Departamento de Matematicas >>> > Universidad del Valle >>> > Calle 13 No. 100 - 00 ; Edificio 320. >>> > Ciudadela Universitaria Melendez >>> > Cali, Colombia >>> > >>> > https://sites.google.com/site/elainepimentel/ >>> > -------------------------------------------------------- >>> > >>> >>> >>> >>> -- >>> 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 >>> >> >> >> >> -- >> Federal University of Rio de Janeiro >> www.cos.ufrj.br/~mario <http://www.cos.ufrj.br/%7Emario> >> > > > > -- > Valeria de Paiva > http://www.cs.bham.ac.uk/~vdp/ > http://valeriadepaiva.org/www/ > -- 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
