Diferència entre les revisions de "Càlcul de superposició"

De L'Enciclopèdia, la wikipedia en valencià
Anar a la navegació Anar a la busca
(Pàgina nova, en el contingut: «El '''càlcul de superposició''' és un càlcul per a Demostració automàtica de teoremes de la lògica equacional de primer orde. Es va dessarrollar en la d...».)
 
m
 
(No es mostren 4 edicions intermiges d'2 usuaris)
Llínea 1: Llínea 1:
El '''càlcul de superposició''' és un càlcul per a Demostració automàtica de teoremes de la lògica equacional de primer orde.  
+
El '''càlcul de superposició''' és un càlcul per a Demostració automàtica de teoremes de la llògica equacional de primer orde.  
  
Es va dessarrollar en la dècada de [[1990]] i combina els conceptes de la resolució de primer orde en la manipulació d'igualtats basades en seqüències ordenades com es dessarrollar en el context de la terminació de Knuth-Bendix.  
+
Es va desenrollar en la [[anys 1990|década de 1990]] i combina els conceptes de la resolució de primer orde en la manipulació d'igualtats basades en seqüències ordenades com es desenrollar en el context de la terminació de Knuth-Bendix.  
  
Pot ser vist com una generalisació de qualsevol resolució (lògica equacional) o terminació constant (lògica clausal completa). Com la majoria dels càlculs de primer orde, la superposició tracta de mostrar la insatisfacibilitat d'un conjunt de clàusules de primer orde, és dir, que realisa proves de refutació.
+
Pot ser vist com una generalisació de qualsevol resolució (llògica equacional) o terminació constant (llògica clausal completa). Com la majoria dels càlculs de primer orde, la superposició tracta de mostrar la insatisfacibilitat d'un conjunt de clàusules de primer orde, és dir, que realisa proves de refutació.  
  
 
[[Categoria: Matemàtiques]]
 
[[Categoria: Matemàtiques]]

Última revisió del 10:50 20 jul 2018

El càlcul de superposició és un càlcul per a Demostració automàtica de teoremes de la llògica equacional de primer orde.

Es va desenrollar en la década de 1990 i combina els conceptes de la resolució de primer orde en la manipulació d'igualtats basades en seqüències ordenades com es desenrollar en el context de la terminació de Knuth-Bendix.

Pot ser vist com una generalisació de qualsevol resolució (llògica equacional) o terminació constant (llògica clausal completa). Com la majoria dels càlculs de primer orde, la superposició tracta de mostrar la insatisfacibilitat d'un conjunt de clàusules de primer orde, és dir, que realisa proves de refutació.