Procedimento de tradução de FOL para FOL com um predicado binário

[Anderson Nakano]

Olá a todos,

Gostaria de saber se alguém de vocês conhece algum procedimento efetivo para traduzir fórmulas da lógica de primeira ordem com um número qualquer de predicados de qualquer aridade para fórmulas da lógica de primeira ordem com apenas um predicado binário.

Há um paper de Kalmar que trata desse assunto (Zurückführung des Entscheidungsproblems auf den Fall von Formeln mit einer einzigen, binären, Funktionsvariablen), mas ele é de 1937, e gostaria de saber se há algo mais recente.

Agradeço desde já,

Anderson

[Marcelo Finger]

Oi Anderson.

Para codificar com um pred TERNÁRIO é razoavelmente simples e até linear.  A partir daí, v vai ter de fazer algum contorcionismo codificante e certamente uma explosão combinatória pra chegar em binário.  Infelizmente fiz as contas de cabeça e não tenho referências.

[]s

--
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+u...@dimap.ufrn.br.
Para ver essa discussão na Web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/2ee173b0-47cf-48a2-94fd-acba527f7961%40dimap.ufrn.br.

--

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

 ORCID: https://orcid.org/0000-0002-1391-1175
 ResearcherID: A-4670-2009