Re: [Logica-l] ATPs (Automatic Theorem Provers) para Lógicas Não-Clássicas

[Joao Marcos]

Walter, e demais colegas:

> Existem ATPs  bacanas para  Lógicas Não-Clássicas?  Para a Logica
> Intuicionista certamente existem, e sei (por trabalhar com tablôs,
> dedução natural, axiomaticas hilbertianas, etc) que certamente  se
> podem adaptar  Isabelle,  Mizar, etc, para isso. Mas eu gostaria de
> saber se há ATPs que são 'nativos'  de   Lógicas Não-Clássicas,e o que
> eles  já demonstraram (se é que...)   de 'surpreendente'.

A lista que a Cláudia mandou é ótima, e o material do Otten que a
Valeria apontou também!  Com relação a demonstradores computacionais
_assistidos por humanos_, o meu atual favorito é de fato o Lean,
desenvolvido pelo Leonardo de Moura.

Como provavelmente seria de se esperar, os demonstradores
_automáticos_ não são em geral construídos para *lógicas* específicas,
mas para *sistemas dedutivos* específicos.  Os dois sistemas online
que eu usei mais recentemente foram:
  MetTel 2 (http://www.mettel-prover.org/demo.php)
  Gen2Sat (http://gen2sat-yonizohar.rhcloud.com/gen2sat/?id=blank)
O MetTel é um demonstrador genérico baseado em *tableaux*, no qual é
bastante fácil definir a sintaxe e as regras da lógica em questão, e
gerar a partir daí um demonstrador "nativo" para esta lógica.  O
Gen2Sat é ainda mais simples de se usar, embora um pouco menos
"customizável", e se baseia em *cálculos de sequente* analíticos,
cujos procedimentos de decisão são traduzidos e enviados para serem
tratados por solucionadores SAT genéricos.

Com relação a demonstrações surpreendentes, acho que isto dependo do
que você entende por "surpreendente"!

Com relação à lógica intuicionista, em particular, a família Loparic
tinha implementado online um demonstrador baseado na semântica de
valorações da Andrea.  Neste momento não estou achando, contudo, o
link para o sistema.  Elaine e Giselle também colocaram online alguns
demonstradores para lógicas lineares e modais.  A Cláudia tem
implementado vários sistemas para lógicas não-clássicas baseados em
resolução.  Certamente elas poderão lhe esclarecer melhor, em primeira
mão, sobre seus trabalhos!

Finalizo acrescentando apenas uma pequena clarificação.  A Valéria escreveu:
>
> George Gonthier, um amigo de muitos anos, e' uma das figuras
> famosas, liderando o time que provou de novo o teorema das 4 Cores

Vale notar, contudo, que o que o Gonthier (Microsoft Research
Cambridge) produziu em 2005 não foi apenas uma nova demonstração do
teorema das quatro cores na qual o computador é usado na sub-tarefa de
checagem exaustiva de um grande número de reduções dos mapas, como
fizeram Appel & Haken na década de 70, mas sim uma demonstração
*inteiramente* produzida com o auxílio de um demonstrador automático
(no caso, o Coq).  Isto consiste no que o Gonthier chama de "formal
program proof", a saber, código que diz não apenas *o quê* a máquina
deve fazer, mas também o *por quê* (entendendo por isto que o código
deve conter uma "computer-checked proof of correctness").

Abraços,
Joao Marcos

-- 
http://sequiturquodlibet.googlepages.com/

-- 
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 postar neste grupo, envie um e-mail para logica-l@dimap.ufrn.br.
Visite este grupo em https://groups.google.com/a/dimap.ufrn.br/group/logica-l/.
Para ver esta discussão na web, acesse 
https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAO6j_Lhc7EFrv86FSYMa2sfYLv3YJ-ERU3V0nu4we_TYGnmgjA%40mail.gmail.com.

Re: [Logica-l] ATPs (Automatic Theorem Provers) para Lógicas Não-Clássicas

[Renata Wassermann]

Para aumentar um pouco a lista:

- Existem montes de provadores para lógicas de descrição de expressividades 
variadas. Alguns estão na lista que a Valéria postou, mas os mais usados - 
HermiT  e Pellet - não estão lá. Uma lista especifica para DLs e ontologias 
pode ser encontrada em 
http://owl.cs.manchester.ac.uk/tools/list-of-reasoners/

- Existem também provadores para lógicas não-monotônicas. O caso de maior 
sucesso em termos de implementação  é ASP (Answer Set Programming), por 
exemplo o Potassco (https://potassco.org/).

Abraços,

Renata.

On Tuesday, April 25, 2017 at 4:11:00 AM UTC-3, Joao Marcos wrote:
>
> Walter, e demais colegas: 
>
> > Existem ATPs  bacanas para  Lógicas Não-Clássicas?  Para a Logica 
> > Intuicionista certamente existem, e sei (por trabalhar com tablôs, 
> > dedução natural, axiomaticas hilbertianas, etc) que certamente  se 
> > podem adaptar  Isabelle,  Mizar, etc, para isso. Mas eu gostaria de 
> > saber se há ATPs que são 'nativos'  de   Lógicas Não-Clássicas,e o que 
> > eles  já demonstraram (se é que...)   de 'surpreendente'. 
>
> A lista que a Cláudia mandou é ótima, e o material do Otten que a 
> Valeria apontou também!  Com relação a demonstradores computacionais 
> _assistidos por humanos_, o meu atual favorito é de fato o Lean, 
> desenvolvido pelo Leonardo de Moura. 
>
> Como provavelmente seria de se esperar, os demonstradores 
> _automáticos_ não são em geral construídos para *lógicas* específicas, 
> mas para *sistemas dedutivos* específicos.  Os dois sistemas online 
> que eu usei mais recentemente foram: 
>   MetTel 2 (http://www.mettel-prover.org/demo.php) 
>   Gen2Sat (http://gen2sat-yonizohar.rhcloud.com/gen2sat/?id=blank) 
> O MetTel é um demonstrador genérico baseado em *tableaux*, no qual é 
> bastante fácil definir a sintaxe e as regras da lógica em questão, e 
> gerar a partir daí um demonstrador "nativo" para esta lógica.  O 
> Gen2Sat é ainda mais simples de se usar, embora um pouco menos 
> "customizável", e se baseia em *cálculos de sequente* analíticos, 
> cujos procedimentos de decisão são traduzidos e enviados para serem 
> tratados por solucionadores SAT genéricos. 
>
> Com relação a demonstrações surpreendentes, acho que isto dependo do 
> que você entende por "surpreendente"! 
>
> Com relação à lógica intuicionista, em particular, a família Loparic 
> tinha implementado online um demonstrador baseado na semântica de 
> valorações da Andrea.  Neste momento não estou achando, contudo, o 
> link para o sistema.  Elaine e Giselle também colocaram online alguns 
> demonstradores para lógicas lineares e modais.  A Cláudia tem 
> implementado vários sistemas para lógicas não-clássicas baseados em 
> resolução.  Certamente elas poderão lhe esclarecer melhor, em primeira 
> mão, sobre seus trabalhos! 
>
> Finalizo acrescentando apenas uma pequena clarificação.  A Valéria 
> escreveu: 
> > 
> > George Gonthier, um amigo de muitos anos, e' uma das figuras 
> > famosas, liderando o time que provou de novo o teorema das 4 Cores 
>
> Vale notar, contudo, que o que o Gonthier (Microsoft Research 
> Cambridge) produziu em 2005 não foi apenas uma nova demonstração do 
> teorema das quatro cores na qual o computador é usado na sub-tarefa de 
> checagem exaustiva de um grande número de reduções dos mapas, como 
> fizeram Appel & Haken na década de 70, mas sim uma demonstração 
> *inteiramente* produzida com o auxílio de um demonstrador automático 
> (no caso, o Coq).  Isto consiste no que o Gonthier chama de "formal 
> program proof", a saber, código que diz não apenas *o quê* a máquina 
> deve fazer, mas também o *por quê* (entendendo por isto que o código 
> deve conter uma "computer-checked proof of correctness"). 
>
> Abraços, 
> Joao Marcos 
>
> -- 
> http://sequiturquodlibet.googlepages.com/ 
>

-- 
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 postar neste grupo, envie um e-mail para logica-l@dimap.ufrn.br.
Visite este grupo em https://groups.google.com/a/dimap.ufrn.br/group/logica-l/.
Para ver esta discussão na web, acesse 
https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/b96a3b25-6fd0-4428-8a26-d9581c2a56fe%40dimap.ufrn.br.

Re: [Logica-l] ATPs (Automatic Theorem Provers) para Lógicas Não-Clássicas

[Walter Carnielli]

Car@s,

Muitíssimo obrigado à Cláudia, Valéria, Renata e João Marcos pelos
excelentes `reports'. Teria levado meses para chegar a isso, se
chegasse!

Aproveito meus agradecimentos para contar, no interesse da Lógica,
porque isso me interessa.

Xavier Caicedo provou em ''The subdirect decomposition theorem for
classes of structures closed under direct limits'' (J. Austral. Math.
Soc. Series 4, 30 (1980), 171-179) uma generalização de um teorema de
Birkhoff, mostrando que toda álgebra  (numa classe K de álgebras
definidas por meio de equações) é um produto subdireto de álgebras
subdiretamente irredutíveis em K.

Há anos e anos atrás, em conversas (nem sei se isso está publicado)
Caicedo me convenceu de que se pudéssemos provar uma versao
construtiva desse fato, isso geraria uma prova sintética do Teorema
das Quatro Cores.

Na Dissertação de Mestrado do Pedro Catuogno de mais de 20 anos
(IMECC) tentamos formalizar isso, e encontrar essa prova ''na unha'',
mas não conseguimos (caso contrário, vocês nos teriam visto na
primeira página do New York TImes) embora algumas coisinhas menores
tivessem saido.

Agora, com esse avanço desconhecido na época, como tenho um ótimo
estudante de Graduação interessadísimo no tema, vamos apoveitar o
embalo...

Não creio que consigamos - mas como me disse o Dória há anos atrás
(talvez ele se lembre) a vida é curta demais para que nos interessemos
pelos problemas fáceis  :-)

Qualquer ajuda, **parceria**,  comentário, puxão de orelha, etc, é
ultra-benvinda(o). Por enquanto só sei arranhar a superfície dos
provadores automáticos...

Abraços,

Walter



Em 25 de abril de 2017 08:59, Renata Wassermann
 escreveu:
> Para aumentar um pouco a lista:
>
> - Existem montes de provadores para lógicas de descrição de expressividades
> variadas. Alguns estão na lista que a Valéria postou, mas os mais usados -
> HermiT  e Pellet - não estão lá. Uma lista especifica para DLs e ontologias
> pode ser encontrada em
> http://owl.cs.manchester.ac.uk/tools/list-of-reasoners/
>
> - Existem também provadores para lógicas não-monotônicas. O caso de maior
> sucesso em termos de implementação  é ASP (Answer Set Programming), por
> exemplo o Potassco (https://potassco.org/).
>
> Abraços,
>
> Renata.
>
> On Tuesday, April 25, 2017 at 4:11:00 AM UTC-3, Joao Marcos wrote:
>>
>> Walter, e demais colegas:
>>
>> > Existem ATPs  bacanas para  Lógicas Não-Clássicas?  Para a Logica
>> > Intuicionista certamente existem, e sei (por trabalhar com tablôs,
>> > dedução natural, axiomaticas hilbertianas, etc) que certamente  se
>> > podem adaptar  Isabelle,  Mizar, etc, para isso. Mas eu gostaria de
>> > saber se há ATPs que são 'nativos'  de   Lógicas Não-Clássicas,e o que
>> > eles  já demonstraram (se é que...)   de 'surpreendente'.
>>
>> A lista que a Cláudia mandou é ótima, e o material do Otten que a
>> Valeria apontou também!  Com relação a demonstradores computacionais
>> _assistidos por humanos_, o meu atual favorito é de fato o Lean,
>> desenvolvido pelo Leonardo de Moura.
>>
>> Como provavelmente seria de se esperar, os demonstradores
>> _automáticos_ não são em geral construídos para *lógicas* específicas,
>> mas para *sistemas dedutivos* específicos.  Os dois sistemas online
>> que eu usei mais recentemente foram:
>>   MetTel 2 (http://www.mettel-prover.org/demo.php)
>>   Gen2Sat (http://gen2sat-yonizohar.rhcloud.com/gen2sat/?id=blank)
>> O MetTel é um demonstrador genérico baseado em *tableaux*, no qual é
>> bastante fácil definir a sintaxe e as regras da lógica em questão, e
>> gerar a partir daí um demonstrador "nativo" para esta lógica.  O
>> Gen2Sat é ainda mais simples de se usar, embora um pouco menos
>> "customizável", e se baseia em *cálculos de sequente* analíticos,
>> cujos procedimentos de decisão são traduzidos e enviados para serem
>> tratados por solucionadores SAT genéricos.
>>
>> Com relação a demonstrações surpreendentes, acho que isto dependo do
>> que você entende por "surpreendente"!
>>
>> Com relação à lógica intuicionista, em particular, a família Loparic
>> tinha implementado online um demonstrador baseado na semântica de
>> valorações da Andrea.  Neste momento não estou achando, contudo, o
>> link para o sistema.  Elaine e Giselle também colocaram online alguns
>> demonstradores para lógicas lineares e modais.  A Cláudia tem
>> implementado vários sistemas para lógicas não-clássicas baseados em
>> resolução.  Certamente elas poderão lhe esclarecer melhor, em primeira
>> mão, sobre seus trabalhos!
>>
>> Finalizo acrescentando apenas uma pequena clarificação.  A Valéria
>> escreveu:
>> >
>> > George Gonthier, um amigo de muitos anos, e' uma das figuras
>> > famosas, liderando o time que provou de novo o teorema das 4 Cores
>>
>> Vale notar, contudo, que o que o Gonthier (Microsoft Research
>> Cambridge) produziu em 2005 não foi apenas uma nova demonstração do
>> teorema das quatro cores na qual o computador é usado na sub-tarefa de
>> checagem exaustiva de um grande número de reduções 

[Logica-l] ainda sobre generalizações de Birkhoff

[Joao Marcos]

2017-04-25 16:37 GMT+02:00 Walter Carnielli:
> Xavier Caicedo provou em ''The subdirect decomposition theorem for
> classes of structures closed under direct limits'' (J. Austral. Math.
> Soc. Series 4, 30 (1980), 171-179) uma generalização de um teorema de
> Birkhoff, mostrando que toda álgebra  (numa classe K de álgebras
> definidas por meio de equações) é um produto subdireto de álgebras
> subdiretamente irredutíveis em K.

Por falar em generalizações de Birkhoff, ocorreu-me postar aqui uma
pergunta que fiz recentemente no StackExchange:
https://math.stackexchange.com/questions/2230920/examples-of-algebraic-structures-that-live-at-the-intersection-of-varieties-and

Se algum dos colegas tiver exemplos a contribuir, seria ótimo!

Abraços,
Joao Marcos

-- 
http://sequiturquodlibet.googlepages.com/

-- 
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 postar neste grupo, envie um e-mail para logica-l@dimap.ufrn.br.
Visite este grupo em https://groups.google.com/a/dimap.ufrn.br/group/logica-l/.
Para ver esta discussão na web, acesse 
https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAO6j_LjC3dg7ONgXwGjJf8YVdAEKrRwx9u0Mv8J5eNHKVsF8Vw%40mail.gmail.com.

[Logica-l] Hubert Dreyfus (1930-2017)

[Marcos Silva]

outra perda recente:

http://dailynous.com/2017/04/24/hubert-dreyfus-1930-2017/

" [it] eventually became Dreyfus’ influential 1972 book What Computers
Can’t Do: A Critique of Artificial Reason. A twenty-year anniversary
edition of the book was published in 1992 under the title What Computers
Still Can’t Do. In this book Dreyfus made a move that became characteristic
of much of his philosophical work. He took the phenomenological account of
human existence—especially as he found it in Heidegger and
Merleau-Ponty—and applied it to influential domains outside of philosophy.."

-- 
Marcos Silva
https://sites.google.com/site/marcossilvarj/
Philosophie macht Spaß!

-- 
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 postar neste grupo, envie um e-mail para logica-l@dimap.ufrn.br.
Visite este grupo em https://groups.google.com/a/dimap.ufrn.br/group/logica-l/.
Para ver esta discussão na web, acesse 
https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAGZ3pzJNxeuHHz27%3D58xJiqZL9-7esC_H84yLZA8Z5tMJKcyXA%40mail.gmail.com.

[Logica-l] Palestras super interessantes na UFRN semana que vem!!

[Elaine Pimentel]

Prezados colegas,

Semana que vem teremos, dentro do nosso grupo de pesquisa Lolita e do nosso
projeto CAPES
AmSud, duas palestras super interessantes: dos Prof. Catuscia Palamidessi
(INRIA Saclay) e Frank Valencia (CNRS).

Ambas serão no anfiteatro A do CCET, 17h. A da Catuscia terça dia 2/05 e a
do Frank quinta dia
4/05. Conforme solicitado a eles, ambos vão fazer apresentações de caráter
geral.

Para quem estiver por perto, a presença é super bem vinda!!!

Abraços, Elaine & Carlos Olarte.


02/04 17h anfiteatro A CCET
Title: Generalized differential privacy and applications to location
privacy

Speaker: Catuscia Palamidessi (INRIA Saclay, France)

Abstract:
Differential Privacy (DP) is one of the most successful approaches to
prevent
disclosure of private information in statistical databases. It provides a
formal privacy
guarantee, ensuring that sensitive information relative to individuals
cannot be
easily inferred by disclosing answers to aggregate queries. If two
databases are
adjacent, i.e. differ  only for an individual, then the query should not
allow
to tell them apart by more than a certain factor. This induces a bound also
on
the distinguishability of two generic databases, which is determined by
their
distance on the Hamming graph of the adjacency relation.

In this talk we lift the restriction on the adjacency relation and we
explore the implications of DP
when the indistinguishability requirement depends on an arbitrary notion of
distance. We show that
we can naturally express, in this way, (protection against) privacy threats
that cannot be
represented with the standard notion, leading to new applications of the DP
framework. We give
intuitive characterizations of these
threats in terms of Bayesian adversaries, which generalize two
interpretations
of (standard) differential privacy from the literature. We revisit the
well-known results  in the
literature of differential privacy stating that universally optimal
mechanisms exist only for counting
queries. We show that, in our extended setting,  universally optimal
mechanisms exist for other
queries too, notably sum, average, and percentile queries.

Finally, we explore an application of our generalized DP to the case of
location privacy. In this
case, the domain consists of the locations on a map and the distance is the
geographical distance.
This instance of the property, that we call  geo-indistinguishability, is a
formal notion of privacy for
location-based systems
that protects the user's exact location, while  allowing approximate
information
-- typically needed to obtain a certain desired service -- to be released.

We describe how to use our mechanism to enhance LBS applications with
geo-indistinguishability guarantees without compromising the quality of the
application results.   It turns out that, among the known mechanisms
independent of the prior, our
mechanism offers the best privacy guarantees. Finally we present a tool,
Location Guard, based on
our framework, that has become quite popular also among the general public.


***
04/04 17h anfiteatro A CCET
Title: An Introduction to the Theory of Concurrent Systems.

Speaker: Frank Valencia (CNRS & LIX, Ecole Polytechnique de Paris,
Universidad Javeriana Cali)

Abstract:

Several modern computational systems consist of multiple processes
computing concurrently,
possibly interacting among each other. This covers a vast variety of
systems which nowadays, due
to technological advances such as the Internet and mobile computing, most
people can easily
relate to. Traditional mathematical models of (sequential) computation
based on functions from
inputs to outputs no longer apply. The crux is that concurrent computation,
e.g., in a reactive
system, is seldom expected to terminate and it involves constant
interaction with the environment.

Concurrency Theory, and in particular process calculi, pioneered by Hoare
and Milner, among
others, is a branch of the theory of computation dealing with concurrent
computation. Process
calculi treat processes much like the lambda-calculus treats computable
functions. They provide a
language in which the structure of term represents the structure of
processes together with an
operational semantics to represent computational  steps.

In this talk I will give a brief introduction to concurrency theory. I will
start from the classical theory
of automata and argue that it is not suitable for reasoning about
concurrent behavior.  I will then
introduce bisimilarity, perhaps the most fundamental equivalence from
concurrency theory.  I will
also describe one of the most representative process calculi for concurrent
behaviour CCS.

-- 
Elaine.
-
Elaine Pimentel  - DMAT/UFRN

Address: Departamento de Matemática
Universidade Federal do Rio Grande do Norte
Campus Universitário - Av. Senador Salgado Filho, s/nº
Lagoa Nova, CEP: 59.078-970 - Natal - RN

Phone: +55 84 3215-3820

http://sites.google.com/site/

[Logica-l] CFP - 3rd FILOMENA Workshop (Quick reminder)

[João Daniel Dantas]

Olá,

Passando aqui para lembrar que o deadline do FILOMENA se encerra nessa
sexta dia 28. Mais informações podem ser encontradas no site
. Agradecemos desde já a ampla
divulgação.

Call for papers:
3rd Workshop on Philosophy, Logic and Analytical Metaphysics
Aug 21-23, 2017
Natal/RN, Brazil

*Extended deadline: April 28*
​
​The third edition of the FILOMENA Workshop (FIlosofia, LOgica e MEtafísica
aNAlítica), promoted by the Group for Logic and Formal Philosophy from the
UFRN, has the purpose of gathering logicians working at the intersection of
Logic and Metaphysics, through the application of formal methods in
Philosophy. Logic, a branch of Philosophy on its own, has outgrown its
original purposes and found connections with other areas of Philosophy,
such as Philosophy of Language, Philosophy of Mathematics, Philosophy of
Science and Philosophy of Mind. Logic has proved to be a powerful tool for
analyzing different philosophical theories, as well as their foundations
and implications; moreover, the birth and development of non-classical
logics has expanded its domain of application much beyond the dreams of its
progenitors.

Topics of interest for our workshop include, but are not limited  to:
Modal metaphysics
Reference and descriptions
Philosophical topics in non-classical logics
Truth-values
Logical consequence
Logical pluralism
Meta-ontology​

The workshop will allow 30 minutes for each contributed talk, divided into
20 minutes for exposition followed by 10 minutes of discussion. The
abstracts may be written in English or Portuguese. Abstracts should have at
most 500 words and should include relevant information about the author
(name, e-mail address, and scientific affiliation). Please submit an
editable file (such as .doc, .odt, .tex) along with a .pdf file of your
abstract. A model of the abstract in .tex is is available at
https://goo.gl/vGzrvb.

This year it is also possible to submit a proposal for a tutorial (two
sessions of 2 hours each). The proposal must indicate the content that will
be presented, along with relevant bibliography. The proposal may be written
in English or Portuguese, should have at most 1000 words and include
relevant information about the author (name, e-mail address, and scientific
affiliation). Please submit an editable file (such as .doc, .odt, .tex)
along with a .pdf file.

Submissions must be sent to the email filomenaworks...@gmail.com by* April
28*, and the authors will be notified of acceptance or rejection by May 15.

After the event, participants will have the chance to submit full papers
for the proceedings of the event, which will be published online in a
blind-reviewed book by the upcoming publisher of PPGFil, the graduate
program of Philosophy from UFRN.

-- 
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 postar neste grupo, envie um e-mail para logica-l@dimap.ufrn.br.
Visite este grupo em https://groups.google.com/a/dimap.ufrn.br/group/logica-l/.
Para ver esta discussão na web, acesse 
https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAKFx%2BYGrvwGi30%2BXPC2zTzUK_A-5oQsT3WV5xsBZjo52G7Z4Tg%40mail.gmail.com.

Re: [Logica-l] ainda sobre generalizações de Birkhoff

[Marcelo Finger]

Walter, JM e demais.

Sobre provas geradas automaticamente, em especial para o caso da
4-coloração, avento a possibilidade de que uma prova automaticamente
gerada (e verificada) possa term MAIS CASOS que a atualmente
conhecida.

Aliás, isso seria o esperado.  Se é fácil gerar e verificar casos, é
provável que seja assim programado.

[]s

Marcelo

PS: Tem os provadores de código aberto gerados pelo meu grupo,
disponíveis para baixar:

a) Para satisfatibilidade probabilística: http://psat.sourceforge.net

b) Para quantificadores de contagem sobre predicados unários:
http://cqu.sourceforge.net

Desculpa o atraso.


2017-04-25 12:58 GMT-03:00 Joao Marcos :
> 2017-04-25 16:37 GMT+02:00 Walter Carnielli:
>> Xavier Caicedo provou em ''The subdirect decomposition theorem for
>> classes of structures closed under direct limits'' (J. Austral. Math.
>> Soc. Series 4, 30 (1980), 171-179) uma generalização de um teorema de
>> Birkhoff, mostrando que toda álgebra  (numa classe K de álgebras
>> definidas por meio de equações) é um produto subdireto de álgebras
>> subdiretamente irredutíveis em K.
>
> Por falar em generalizações de Birkhoff, ocorreu-me postar aqui uma
> pergunta que fiz recentemente no StackExchange:
> https://math.stackexchange.com/questions/2230920/examples-of-algebraic-structures-that-live-at-the-intersection-of-varieties-and
>
> Se algum dos colegas tiver exemplos a contribuir, seria ótimo!
>
> Abraços,
> Joao Marcos
>
> --
> http://sequiturquodlibet.googlepages.com/
>
> --
> 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 postar neste grupo, envie um e-mail para logica-l@dimap.ufrn.br.
> Visite este grupo em 
> https://groups.google.com/a/dimap.ufrn.br/group/logica-l/.
> Para ver esta discussão na web, acesse 
> https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAO6j_LjC3dg7ONgXwGjJf8YVdAEKrRwx9u0Mv8J5eNHKVsF8Vw%40mail.gmail.com.



-- 
 Marcelo Finger
 Departament of Computer Science, IME
 University of Sao Paulo
 http://www.ime.usp.br/~mfinger

-- 
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 postar neste grupo, envie um e-mail para logica-l@dimap.ufrn.br.
Visite este grupo em https://groups.google.com/a/dimap.ufrn.br/group/logica-l/.
Para ver esta discussão na web, acesse 
https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CABqmzx1JXk_bqZsjd8ONfpu3hLBZtRc4YbWUL89tcH0Q_wMdwA%40mail.gmail.com.

Re: [Logica-l] ATPs (Automatic Theorem Provers) para Lógicas Não-Clássicas

[Joao Marcos]

2017-04-26 2:55 GMT+02:00 Marcelo Finger :
>
> Sobre provas geradas automaticamente, em especial para o caso da
> 4-coloração, avento a possibilidade de que uma prova automaticamente
> gerada (e verificada) possa term MAIS CASOS que a atualmente
> conhecida.
>
> Aliás, isso seria o esperado.  Se é fácil gerar e verificar casos, é
> provável que seja assim programado.

Confesso que não sei dizer se a demonstração automatizada tem mais
casos do que os que seriam previstos...  Na demonstração original de
Appel & Haken [1976] havia 1936 mapas "minimais" com 5 cores a
analisar (a estratégia da demonstração, seguindo a ideia principal da
demonstração errada publicada por Kempe em 1879, é justamente a do
raciocínio por absurdo, mostrando que cada uma destas configurações
pode ser reduzida a uma configuração menor que ainda necessitaria 5
cores).  Em 1996, Robertson et al mostraram que é possível diminuir o
número de casos a considerar para "apenas" 633 configurações.  Até
onde sei, foi esta última versão da demonstração que foi formalizada
pelo Gonthier.

Abraços,
Joao Marcos

-- 
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 postar neste grupo, envie um e-mail para logica-l@dimap.ufrn.br.
Visite este grupo em https://groups.google.com/a/dimap.ufrn.br/group/logica-l/.
Para ver esta discussão na web, acesse 
https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAO6j_LgphyNLZSRJyrfmMzga7UtRebWyyc7gZL6m%2BHWPpdTruQ%40mail.gmail.com.