anldp - Online di Cloud

PROGRAM:

NAMA

anldp - implementasi prosedur kepuasan proposisional Davis-Putnam

RINGKASAN

danlp [Pilihan] file masukan > berkas keluaran

DESKRIPSI

Halaman manual ini mendokumentasikan secara singkat danlp perintah.

danlp adalah implementasi dari prosedur Davis-Putnam untuk proposisional
masalah kepuasan. danlp memaparkan prosedur yang digunakan oleh gada2(1) untuk menentukan
kepuasan. danlp juga dapat mengambil pernyataan dalam logika orde pertama dengan kesetaraan dan a
ukuran domain n lalu cari model ukuran n. Kode pencarian model orde pertama
mengubah pernyataan menjadi set klausa proposisi sedemikian rupa sehingga orde pertama
pernyataan memiliki model ukuran n jika dan hanya jika klausa proposisi adalah
memuaskan. Himpunan proposisional kemudian diberikan ke kode Davis-Putnam; setiap
model proposisional yang ditemukan dapat diterjemahkan ke model orde pertama
pernyataan. Program pencarian model orde pertama menerima pernyataan hanya dalam bentuk yang diratakan
bentuk klausa relasional tanpa simbol fungsi.

PILIHAN

-s Lakukan subsumsi. (Subsumption selalu dilakukan selama unit preprocessing.)

-p Cetak model seperti yang ditemukan.

-m n Berhenti ketika nmodel th ditemukan.

-t n Berhenti setelah n detik.

-k n Alokasikan paling banyak n kbytes untuk penyimpanan klausa.

-x n Eksperimen grup kuasi n.

-B fillet
Pencadangan tugas ke file.

-b n Buat cadangan tugas setiap n detik.

-R fillet
Pulihkan tugas dari file. File biasanya hanya berisi baris terakhir dari
file cadangan. Masukan lain, khususnya klausa, harus diberikan persis seperti pada
pencarian asli.

-n n Opsi ini digunakan untuk pencarian model orde pertama. Parameternya n menentukan
ukuran domain, dan kehadirannya memberi tahu program untuk membaca orde pertama yang diratakan
klausa input relasional alih-alih klausa proposisional.

Gunakan anldp online menggunakan layanan onworks.net