Visão Geral dos Provadores Automáticos de Teoremas - Histórico de revisão

Adolfo: /* O que é Prova Automática de Teoremas? */

2009-04-24T14:08:32Z

O que é Prova Automática de Teoremas?

Adolfo: /* Siglas */

2009-04-24T14:08:21Z

Siglas

Adolfo: /* O que é Prova Automática de Teoremas */

2009-04-24T14:08:12Z

O que é Prova Automática de Teoremas

Adolfo: /* O que é Prova Automática de Teoremas */

2009-04-24T14:08:03Z

O que é Prova Automática de Teoremas

Adolfo em 14h07min de 24 de abril de 2009

2009-04-24T14:07:55Z

Adolfo: /* Para que a Prova Automática de Teoremas tem sido realmente útil? */

2009-04-24T14:01:28Z

Para que a Prova Automática de Teoremas tem sido realmente útil?

Adolfo em 13h49min de 24 de abril de 2009

2009-04-24T13:49:57Z

Adolfo em 13h49min de 24 de abril de 2009

2009-04-24T13:49:36Z

Adolfo: Nova página: Tradução e Adaptação do texto de Geoff Sutcliffe, disponível em http://www.cs.miami.edu/~tptp/OverviewOfATP.html

2009-04-24T13:44:19Z

Nova página: Tradução e Adaptação do texto de Geoff Sutcliffe, disponível em http://www.cs.miami.edu/~tptp/OverviewOfATP.html

Nova página

Tradução e Adaptação do texto de Geoff Sutcliffe, disponível em http://www.cs.miami.edu/~tptp/OverviewOfATP.html

@@ Linha 7: / Linha 7: @@
 = O que é Prova Automática de Teoremas? =
-Prova Automática de Teoremas (''Automated Theorem Proving'' ou ATP) trata do desenvolvimento de programas de computador que mostram que cerca de afirmação (a conjectura) é uma consequência lógica de um conjunto de afirmações (os axiomas e hipóteses). Sistemas de ATP são utilizados em uma ampla variedade de domínios. Por exemplo, um matemático poderia provar a conjectura de que grupos de ordem dois são comutativos, a partir dos axiomas da teoria dos grupos; um consultor de gestão poderia formular axiomas que descrevem como as organizações crescem e interagem, e a partir destes axiomas provar que as taxas de óbito organizacional diminuem com a idade; um desenvolvedor de hardware poderia validar a concepção de um circuito provando uma conjectura que descreve o desempenho do circuito, dados axiomas que descrevem o circuito em si, ou um adolescente frustrado pode formular as  faces  misturadas de um cubo Rubik como uma conjectura e provar, a partir de axiomas que descrevem mudanças legais para a configuração do cubo, que o cubo pode ser reajustado para o estado de solução. Todas estas são tarefas que podem ser executadas por um sistema de ATP, dada uma adequada formulação do problema como axiomas, hipóteses, e uma conjectura.
+Prova Automática de Teoremas (''Automated Theorem Proving'' ou '''ATP''') trata do desenvolvimento de programas de computador que mostram que cerca de afirmação (a conjectura) é uma consequência lógica de um conjunto de afirmações (os axiomas e hipóteses). Sistemas de ATP são utilizados em uma ampla variedade de domínios. Por exemplo, um matemático poderia provar a conjectura de que grupos de ordem dois são comutativos, a partir dos axiomas da teoria dos grupos; um consultor de gestão poderia formular axiomas que descrevem como as organizações crescem e interagem, e a partir destes axiomas provar que as taxas de óbito organizacional diminuem com a idade; um desenvolvedor de hardware poderia validar a concepção de um circuito provando uma conjectura que descreve o desempenho do circuito, dados axiomas que descrevem o circuito em si, ou um adolescente frustrado pode formular as  faces  misturadas de um cubo Rubik como uma conjectura e provar, a partir de axiomas que descrevem mudanças legais para a configuração do cubo, que o cubo pode ser reajustado para o estado de solução. Todas estas são tarefas que podem ser executadas por um sistema de ATP, dada uma adequada formulação do problema como axiomas, hipóteses, e uma conjectura.
 (...)

← Versão anterior		Edição de 14h08min de 24 de abril de 2009
Linha 3:		Linha 3:
	(...)		(...)

−	~~== Siglas ==~~

−	~~ATP =~~

−
−
	= O que é Prova Automática de Teoremas? =		= O que é Prova Automática de Teoremas? =

← Versão anterior		Edição de 14h08min de 24 de abril de 2009
Linha 9:		Linha 9:


−	= O que é Prova Automática de Teoremas =	+	= O que é Prova Automática de Teoremas? =

	Prova Automática de Teoremas (''Automated Theorem Proving'' ou ATP) trata do desenvolvimento de programas de computador que mostram que cerca de afirmação (a conjectura) é uma consequência lógica de um conjunto de afirmações (os axiomas e hipóteses). Sistemas de ATP são utilizados em uma ampla variedade de domínios. Por exemplo, um matemático poderia provar a conjectura de que grupos de ordem dois são comutativos, a partir dos axiomas da teoria dos grupos; um consultor de gestão poderia formular axiomas que descrevem como as organizações crescem e interagem, e a partir destes axiomas provar que as taxas de óbito organizacional diminuem com a idade; um desenvolvedor de hardware poderia validar a concepção de um circuito provando uma conjectura que descreve o desempenho do circuito, dados axiomas que descrevem o circuito em si, ou um adolescente frustrado pode formular as faces misturadas de um cubo Rubik como uma conjectura e provar, a partir de axiomas que descrevem mudanças legais para a configuração do cubo, que o cubo pode ser reajustado para o estado de solução. Todas estas são tarefas que podem ser executadas por um sistema de ATP, dada uma adequada formulação do problema como axiomas, hipóteses, e uma conjectura.		Prova Automática de Teoremas (''Automated Theorem Proving'' ou ATP) trata do desenvolvimento de programas de computador que mostram que cerca de afirmação (a conjectura) é uma consequência lógica de um conjunto de afirmações (os axiomas e hipóteses). Sistemas de ATP são utilizados em uma ampla variedade de domínios. Por exemplo, um matemático poderia provar a conjectura de que grupos de ordem dois são comutativos, a partir dos axiomas da teoria dos grupos; um consultor de gestão poderia formular axiomas que descrevem como as organizações crescem e interagem, e a partir destes axiomas provar que as taxas de óbito organizacional diminuem com a idade; um desenvolvedor de hardware poderia validar a concepção de um circuito provando uma conjectura que descreve o desempenho do circuito, dados axiomas que descrevem o circuito em si, ou um adolescente frustrado pode formular as faces misturadas de um cubo Rubik como uma conjectura e provar, a partir de axiomas que descrevem mudanças legais para a configuração do cubo, que o cubo pode ser reajustado para o estado de solução. Todas estas são tarefas que podem ser executadas por um sistema de ATP, dada uma adequada formulação do problema como axiomas, hipóteses, e uma conjectura.

← Versão anterior		Edição de 14h08min de 24 de abril de 2009
Linha 13:		Linha 13:
	Prova Automática de Teoremas (''Automated Theorem Proving'' ou ATP) trata do desenvolvimento de programas de computador que mostram que cerca de afirmação (a conjectura) é uma consequência lógica de um conjunto de afirmações (os axiomas e hipóteses). Sistemas de ATP são utilizados em uma ampla variedade de domínios. Por exemplo, um matemático poderia provar a conjectura de que grupos de ordem dois são comutativos, a partir dos axiomas da teoria dos grupos; um consultor de gestão poderia formular axiomas que descrevem como as organizações crescem e interagem, e a partir destes axiomas provar que as taxas de óbito organizacional diminuem com a idade; um desenvolvedor de hardware poderia validar a concepção de um circuito provando uma conjectura que descreve o desempenho do circuito, dados axiomas que descrevem o circuito em si, ou um adolescente frustrado pode formular as faces misturadas de um cubo Rubik como uma conjectura e provar, a partir de axiomas que descrevem mudanças legais para a configuração do cubo, que o cubo pode ser reajustado para o estado de solução. Todas estas são tarefas que podem ser executadas por um sistema de ATP, dada uma adequada formulação do problema como axiomas, hipóteses, e uma conjectura.		Prova Automática de Teoremas (''Automated Theorem Proving'' ou ATP) trata do desenvolvimento de programas de computador que mostram que cerca de afirmação (a conjectura) é uma consequência lógica de um conjunto de afirmações (os axiomas e hipóteses). Sistemas de ATP são utilizados em uma ampla variedade de domínios. Por exemplo, um matemático poderia provar a conjectura de que grupos de ordem dois são comutativos, a partir dos axiomas da teoria dos grupos; um consultor de gestão poderia formular axiomas que descrevem como as organizações crescem e interagem, e a partir destes axiomas provar que as taxas de óbito organizacional diminuem com a idade; um desenvolvedor de hardware poderia validar a concepção de um circuito provando uma conjectura que descreve o desempenho do circuito, dados axiomas que descrevem o circuito em si, ou um adolescente frustrado pode formular as faces misturadas de um cubo Rubik como uma conjectura e provar, a partir de axiomas que descrevem mudanças legais para a configuração do cubo, que o cubo pode ser reajustado para o estado de solução. Todas estas são tarefas que podem ser executadas por um sistema de ATP, dada uma adequada formulação do problema como axiomas, hipóteses, e uma conjectura.

		+	(...)

	= Para que a Prova Automática de Teoremas tem sido realmente útil? =		= Para que a Prova Automática de Teoremas tem sido realmente útil? =

← Versão anterior		Edição de 14h07min de 24 de abril de 2009
Linha 5:		Linha 5:
	== Siglas ==		== Siglas ==

−	ATP = ~~''Automated Theorem Proving'' (Prova Automática de Teoremas)~~	+	ATP =

		+
		+
		+	= O que é Prova Automática de Teoremas =
		+
		+	Prova Automática de Teoremas (''Automated Theorem Proving'' ou ATP) trata do desenvolvimento de programas de computador que mostram que cerca de afirmação (a conjectura) é uma consequência lógica de um conjunto de afirmações (os axiomas e hipóteses). Sistemas de ATP são utilizados em uma ampla variedade de domínios. Por exemplo, um matemático poderia provar a conjectura de que grupos de ordem dois são comutativos, a partir dos axiomas da teoria dos grupos; um consultor de gestão poderia formular axiomas que descrevem como as organizações crescem e interagem, e a partir destes axiomas provar que as taxas de óbito organizacional diminuem com a idade; um desenvolvedor de hardware poderia validar a concepção de um circuito provando uma conjectura que descreve o desempenho do circuito, dados axiomas que descrevem o circuito em si, ou um adolescente frustrado pode formular as faces misturadas de um cubo Rubik como uma conjectura e provar, a partir de axiomas que descrevem mudanças legais para a configuração do cubo, que o cubo pode ser reajustado para o estado de solução. Todas estas são tarefas que podem ser executadas por um sistema de ATP, dada uma adequada formulação do problema como axiomas, hipóteses, e uma conjectura.

← Versão anterior		Edição de 14h01min de 24 de abril de 2009
Linha 10:		Linha 10:

	= Para que a Prova Automática de Teoremas tem sido realmente útil? =		= Para que a Prova Automática de Teoremas tem sido realmente útil? =
−
−	Many significant problems have been, and continue to be, solved using ATP. The fields where the most notable successes have been achieved are mathematics, software creation and verification, and hardware verification, and knowledge based systems.
−
−	The most exciting recent success in mathematics has been the settling of the Robbins problem by the ATP system EQP. In 1933 Herbert Robbins conjectured that a particular group of axioms form a basis for Boolean algebra, but neither he nor anyone else (until the solution by EQP) could prove this. The proof that confirms that Robbins' axioms are a basis for Boolean algebra was found October 10, 1996, after about 8 days of search by EQP, on an RS/6000 processor. This result was reported in the New York Times.

	Muitos problemas significativos foram, e continuam a ser resolvidos por meio ATP. Os campos onde os sucessos mais notáveis foram atingidos são matemática, criação e verificação de software, e verificação de hardware, e sistemas baseados em conhecimento.		Muitos problemas significativos foram, e continuam a ser resolvidos por meio ATP. Os campos onde os sucessos mais notáveis foram atingidos são matemática, criação e verificação de software, e verificação de hardware, e sistemas baseados em conhecimento.

@@ Linha 2: / Linha 2: @@
 (...)
 ATP = ''Automated Theorem Proving'' (Prova Automática de Teoremas)
 Para que a Prova Automática de Teoremas tem sido realmente útil?
 Many significant problems have been, and continue to be, solved using ATP. The fields where the most notable successes have been achieved are mathematics, software creation and verification, and hardware verification, and knowledge based systems.

← Versão anterior		Edição de 13h49min de 24 de abril de 2009
Linha 1:		Linha 1:
		+	(em construção)
		+
		+	(...)
		+
		+	ATP = ''Automated Theorem Proving'' (Prova Automática de Teoremas)
		+
		+	Para que a Prova Automática de Teoremas tem sido realmente útil?
		+
		+	Many significant problems have been, and continue to be, solved using ATP. The fields where the most notable successes have been achieved are mathematics, software creation and verification, and hardware verification, and knowledge based systems.
		+
		+	The most exciting recent success in mathematics has been the settling of the Robbins problem by the ATP system EQP. In 1933 Herbert Robbins conjectured that a particular group of axioms form a basis for Boolean algebra, but neither he nor anyone else (until the solution by EQP) could prove this. The proof that confirms that Robbins' axioms are a basis for Boolean algebra was found October 10, 1996, after about 8 days of search by EQP, on an RS/6000 processor. This result was reported in the New York Times.
		+
		+	Muitos problemas significativos foram, e continuam a ser resolvidos por meio ATP. Os campos onde os sucessos mais notáveis foram atingidos são matemática, criação e verificação de software, e verificação de hardware, e sistemas baseados em conhecimento.
		+
		+	O mais recente e emocionante sucesso em matemática foi a resolução do problema de Robbins pelo sistema de ATP "EQP". Em 1933 Herbert Robbins conjecturou que um grupo particular de axiomas formam uma base para uma ágebra booleana, mas nem ele nem qualquer outra pessoa (até que a solução foi obtida pelo sistema EQP) conseguiu provar isso. A prova que confirma que os axiomas de Robbins são uma base para uma álgebra booleana foi encontrada em 10 de outubro de 1996, após cerca de 8 dias de busca pelo EQP, em um processador RS/6000. Este [http://www.nytimes.com/library/cyber/week/1210math.html resultado foi relatado no New York Times].
		+
		+
		+	(...)

	Tradução e Adaptação do texto de Geoff Sutcliffe, disponível em http://www.cs.miami.edu/~tptp/OverviewOfATP.html		Tradução e Adaptação do texto de Geoff Sutcliffe, disponível em http://www.cs.miami.edu/~tptp/OverviewOfATP.html