Click for new scientific resources and news about Corona[COVID-19]

Paper Information

Title: 

AN ALGORITHM TO VERIFY FORMULAS BY MEANS OF (0,S,=)-BDDS

Type: PAPER
Author(s): BADBAN BAHAREH,DE POL JACO VAN
 
 
 
Name of Seminar: CONFRANCE SALANE ANJOMANE COMPUTER IRAN
Type of Seminar:  CONFERENCE
Sponsor:  Anjomane Computer Iran
Date:  2004Volume 9
 
 
Abstract: 

IN THIS ARTICLE WE PROVIDE AN ALGORITHM TO VERIFY FORMULAS OF THE FRAGMENT OF RST ORDER LOGIC, CONSISTING OF QUANTI ER FREE LOGIC WITH ZERO, SUCCESSOR AND EQUALITY. WE RST DEVELOP A REWRITE SYSTEM TO EXTRACT AN EQUIVALENT ORDERED (0,S,=)-BDD FROM ANY GIVEN (0,S,=)-BDD. THEN WE SHOW COMPLETENESS OF THE REWRITE SYSTEM. FINALLY WE MAKE AN ALGORITHM WITH THE SAME RESULT AS THE REWRITE SYSTEM. GIVEN AN ORDERED (0,S,=)-BDDS WE ARE ABLE TO SEE IN CONSTANT TIME WHETHER THE FORMULA IS A TAUTOLOGY, A CONTRADICTION, OR ONLY SATIS ABLE.

 
Keyword(s): ALGORITHM, DECISION DIAGRAMS, EQUALITY, THEOREM PROVING, DECISION PROCEDURE, NATU- RAL NUMBERS
 
 
Yearly Visit 39   pdf-file tarjomyar
 
Latest on Blog
Enter SID Blog