Theorem Prover on Propositions in Finite Domains 
Author Message
 Theorem Prover on Propositions in Finite Domains

Hello,

I am looking for an efficient algorithm that finds all solutions (if
any) to a logical proposition (with operators AND, OR and NOT) in
which all atoms are of the form : <attribute> is_element_of <set>

The solution should be stated as a dual clause like :

attrib1 is_element_of set1 AND NOT attrib2 is_element_of set2 AND ...

in which set1, set2 etc. are nonempty sets
(attribx is_element_of EMPTYSET is equivalent to FALSE),
and all attrib1, attrib2 etc. are distinct.

Of course there are simple algorithms that can convert any proposition
to dual clause normal form. The expressions however I am dealing with
are huge. I need an efficient algorithm to beat the combinatorial
effects.

Could you set me on the right track regarding a theory or possible
even an algorithm preferably in Prolog?

Jan van der Vorst



Sun, 07 Nov 1999 03:00:00 GMT  
 Theorem Prover on Propositions in Finite Domains


:
: I am looking for an efficient algorithm that finds all solutions (if
: any) to a logical proposition (with operators AND, OR and NOT) in
: which all atoms are of the form : <attribute> is_element_of <set>
:
: The solution should be stated as a dual clause like :
:
: attrib1 is_element_of set1 AND NOT attrib2 is_element_of set2 AND ...
:
: in which set1, set2 etc. are nonempty sets
: (attribx is_element_of EMPTYSET is equivalent to FALSE),
: and all attrib1, attrib2 etc. are distinct.
:
: Of course there are simple algorithms that can convert any proposition
: to dual clause normal form. The expressions however I am dealing with
: are huge. I need an efficient algorithm to beat the combinatorial
: effects.
:
: Could you set me on the right track regarding a theory or possible
: even an algorithm preferably in Prolog?
:

You can use Davis-Putnam like algorithm for generating satisfying
valuations of a formula.

  M. Davis, H. Putnam. A computing procedure for quantification
  theory. J. Assoc. Comput. Mach., 1960, 7. pp. 201-215.

That is you choose recursively Boolean variables from the formula,
instantiate them with values {true,false} and propagate the values
into the formula.

--

Institute of Computer Science, Tartu University
http://www.cs.ut.ee/~tqnu/



Sun, 14 Nov 1999 03:00:00 GMT  
 Theorem Prover on Propositions in Finite Domains


:
: I am looking for an efficient algorithm that finds all solutions (if
: any) to a logical proposition (with operators AND, OR and NOT) in
: which all atoms are of the form : <attribute> is_element_of <set>
:
: The solution should be stated as a dual clause like :
:
: attrib1 is_element_of set1 AND NOT attrib2 is_element_of set2 AND ...
:
: in which set1, set2 etc. are nonempty sets
: (attribx is_element_of EMPTYSET is equivalent to FALSE),
: and all attrib1, attrib2 etc. are distinct.
:
: Of course there are simple algorithms that can convert any proposition
: to dual clause normal form. The expressions however I am dealing with
: are huge. I need an efficient algorithm to beat the combinatorial
: effects.
:
: Could you set me on the right track regarding a theory or possible
: even an algorithm preferably in Prolog?
:

You can use Davis-Putnam like algorithm for generating satisfying
valuations of a formula.

  M. Davis, H. Putnam. A computing procedure for quantification
  theory. J. Assoc. Comput. Mach., 1960, 7. pp. 201-215.

That is you choose recursively Boolean variables from the formula,
instantiate them with values {true,false} and propagate the values
into the formula.

--

Institute of Computer Science, Tartu University
http://www.cs.ut.ee/~tqnu/



Sun, 14 Nov 1999 03:00:00 GMT  
 
 [ 3 post ] 

 Relevant Pages 

1. Theorem provers

2. Theorem prover recommendation?

3. Theorem Prover/Reason maintenance System

4. SUMMARY: Theorem provers and simplifiers for Presburger

5. Theorem provers & simplifiers for Presburger arithmetic

6. Q: Prolog, sets of instances, theorem prover

7. Theorem prover and geometry

8. THEOREM-PROVER in FORTH wanted (based on LAWS OF FORM)

9. Predicate logic theorem prover

10. Theorem provers in Prolog

11. leanTAP theorem prover

12. PROLOG implementations of Theorem Provers

 

 
Powered by phpBB® Forum Software