|
Abstract:
|
This dissertation is about the development of a parallel software system for
representing and solving problems of finite model theory and its application.
The theoretical foundation of the system is presented, as well as an in-depth
explanation of the implementation in Python. In particular, a parallel method
for computing Boolean expressions based on the properties of finite free
Boolean algebras is developed. It is also shown how various finite
combinatorial objects can be coded in the formalism of Boolean algebras and
counted by this procedure. Specifically, using a translation of first order
predicate formulas to propositional formulas, we developed a technique for
constructing and counting finite models of first order theories. Finally, we
have developed some general techniques that enable more effective use of
our system. We illustrate these techniques on two examples. The first one
deals with partial orders, while the other one is about random graphs. |