Apa itu Automated Reasoning?
Automated reasoning adalah bidang dalam ilmu komputer yang berkaitan dengan penerapan penalaran dalam bentuk logika ke sistem komputasi. Jika diberikan serangkaian asumsi dan tujuan, sistem automated reasoning harus mampu membuat inferensi logis menuju tujuan tersebut secara otomatis. Komputer yang menggunakan automated reasoning dapat digunakan untuk mengotomatiskan dan menerapkan penalaran logis ke aktivitas seperti pembuktian teorema, pemeriksaan bukti, atau perancangan sirkuit. Automated reasoning juga dapat menggunakan logika dalam bentuk penalaran melalui analogi, induksi, abduksi, dan penalaran nonmonotonik. Namun, istilah automated reasoning paling sering digunakan dalam konteks penalaran deduktif dalam matematika dan logika.
Istilah “domain masalah” digunakan untuk menggambarkan kelas masalah yang disajikan kepada program automated reasoning. Domain masalah mencakup asumsi masalah, yaitu pernyataan yang memberikan informasi relevan kepada sistem automated reasoning, dan kesimpulan masalah, yaitu pertanyaan yang diajukan kepada sistem. Program penalaran akan menerima domain masalah sebagai masukan dan memberikan solusi sebagai keluaran, seperti validitas suatu bukti. Program automated reasoning akan berhenti ketika solusi ditemukan atau sumber daya habis.
Penggunaan paling umum dari program automated reasoning adalah untuk membuktikan teorema, yang dilakukan dengan menyediakan deskripsi algoritmik terhadap kalkulus yang digunakan. Pengguna juga harus menentukan kelas masalah yang perlu diselesaikan oleh program automated reasoning, bahasa yang akan digunakan program untuk merepresentasikan informasi yang diberikan, serta metode yang digunakan program untuk mengimplementasikan inferensi deduktif.
Istilah automated deduction juga dapat digunakan untuk merujuk pada automated reasoning. Namun, automated deduction lebih sempit dalam penggunaannya, yaitu merujuk pada penggunaan logika deduktif dalam matematika.
Penggunaan
Automated reasoning paling sering digunakan dengan penalaran deduktif untuk menemukan, memeriksa, dan memverifikasi bukti matematis menggunakan sistem komputasi. Menggunakan sistem automated reasoning untuk memeriksa bukti memastikan bahwa pengguna tidak membuat kesalahan dalam perhitungannya. Automated reasoning juga dapat digunakan untuk aplikasi dalam matematika, teknik, ilmu komputer, atau tujuan non-matematis. Namun, banyak dari subjek lain ini tetap harus direpresentasikan menggunakan bahasa yang dapat dipahami oleh program.
Automated Reasoning dan AI
Automated reasoning dianggap sebagai subbidang kecerdasan buatan (AI). Namun, metode dan implementasi keduanya cukup unik sehingga dapat dianggap sebagai entitas yang terpisah. Misalnya, AI biasanya menggunakan jenis logika yang disebut logika modal, yang menggunakan logika klasik sambil juga mengekspresikan modalitas (kemungkinan atau ketidakmungkinan). Istilah AI juga memiliki konotasi yang menunjukkan komputer yang bekerja seperti manusia, berbeda dengan cara kerja automated reasoning.