anthem 1

เพลงสรรเสริญ

แปลโปรแกรมชุดคำตอบเป็นภาษาพิสูจน์ทฤษฎีบทอันดับหนึ่ง

สถานะของโครงการนี้

บันทึก

ขณะนี้คุณกำลังดู anthem เวอร์ชัน 1 ซึ่งสร้างโดย Patrick Lühne และไม่ได้ได้รับการพัฒนาอีกต่อไป จะไม่มีการดำเนินการใดๆ ต่อพื้นที่เก็บข้อมูลนี้อีกต่อไป

หากคุณสนใจเพลงสรรเสริญเวอร์ชันล่าสุด โปรดดูที่พื้นที่เก็บข้อมูลใหม่

ภาพรวม

anthem แปลโปรแกรม ASP (ในภาษาอินพุตของ clingo ) เป็นภาษาของผู้พิสูจน์ทฤษฎีบทอันดับหนึ่งเช่น Prover9

การใช้งาน

เพื่อตรวจสอบว่าโปรแกรมใช้ข้อกำหนดให้เรียกใช้เพลงสรรเสริญ anthem โดยใช้คำสั่ง verify-program :

 $ เพลงยืนยันโปรแกรม <ไฟล์โปรแกรม> <ไฟล์ข้อมูลจำเพาะ>...

โปรดทราบว่าอาจมีการระบุไฟล์ข้อกำหนดหลายไฟล์ สิ่งนี้มีประโยชน์สำหรับการแยกบทแทรกและสัจพจน์ออกจากสมมติฐานและข้อกำหนด

ตัวอย่างการคำนวณค่าพื้นของรากที่สองของตัวเลขสามารถทำซ้ำได้ดังนี้:

 $ ตัวอย่างโปรแกรมตรวจสอบเพลงสรรเสริญพระบารมี / ตัวอย่าง -2. {lp, spec, บทแทรก}

สัญกรณ์วงเล็บปีกกาเป็นการชวเลขของ Bash

 $ เพลงตรวจสอบโปรแกรม examples/example-2.lp examples/example-2.spec examples/example-2.lemmas

ตามค่าเริ่มต้น anthem สรรเสริญพระบารมีจะทำให้คลาร์กดำเนินการเสร็จสิ้นในสูตรที่แปล ตรวจสอบว่าตัวแปรใดเป็นจำนวนเต็ม และทำให้เอาต์พุตง่ายขึ้นโดยใช้กฎการแปลงพื้นฐานหลายข้อ

ขั้นตอนการประมวลผลเหล่านี้สามารถปิดได้ด้วยตัวเลือก --no-complete , --no-simplify และ --no-detect-integers

อาคาร

anthem สร้างขึ้นด้วยเครื่องมือ cargo ของ Rust หลังจากติดตั้ง Rust แล้ว สามารถสร้าง anthem ได้ดังนี้:

 $ git โคลน https://github.com/potassco/anthem.git
เพลงซีดี $
$ cargo build --release

ไบนารี anthem จะพร้อมใช้งานในไดเร็กทอรี target/release/ อีกทางหนึ่ง สามารถเรียกใช้ anthem ได้โดยใช้ cargo ดังนี้:

 $ cargo run -- Verify-program <ไฟล์โปรแกรม> <ไฟล์ข้อมูลจำเพาะ>...

ผู้ร่วมให้ข้อมูล

• แพทริค ลือห์เน