Geoutomatiseerde redenering

In rekenaarwetenskap, veral in kennisvoorstelling en redenering en metalogieka, word die gebied van geoutomatiseerde redenering gewy aan die verstaan van verskillende aspekte van redenering. Die studie van geoutomatiseerde redenering help om rekenaarprogramme te produseer wat rekenaars toelaat om heeltemal, of amper heeltemal, outomaties te redeneer. Alhoewel geoutomatiseerde redenering as 'n subveld van kunsmatige intelligensie beskou word, het dit ook verbande met teoretiese rekenaarwetenskap en filosofie.

Die mees ontwikkelde subareas van geoutomatiseerde redenering is outomatiese stellingbewys (en die minder geoutomatiseerde maar meer pragmatiese subveld van interaktiewe stellingbewys) en outomatiese bewyskontrole (wat beskou word as gewaarborgde korrekte redenasie onder vaste aannames). Uitgebreide werk is gedoen in redenering deur analogie met gebruikmaking van induksie en abduksie.

Ander belangrike onderwerpe sluit in redenering onder onsekerheid en nie-monotoniese redenering. 'n Belangrike deel van die onsekerheidsveld is dié van argumentasie, waar verdere beperkings van minimaliteit en konsekwentheid bo-op die meer standaard outomatiese afleiding toegepas word. John Pollock se OSCAR-stelsel is 'n voorbeeld van 'n geoutomatiseerde argumentasiestelsel wat meer spesifiek is as om net 'n outomatiese stellingbewyser te wees.

Gereedskap en tegnieke van geoutomatiseerde redenering sluit in die klassieke logika en berekeninge, wasige logika, Bayesiaanse afleidings, redenering met maksimale entropie en baie minder formele ad hoc tegnieke.