6 resultados para satisfiability modulo theories
em Bulgarian Digital Mathematics Library at IMI-BAS
Resumo:
In the present paper we investigate the life cycles of formalized theories that appear in decision making instruments and science. In few words mixed theories are build in the following steps: Initially a small collection of facts is the kernel of the theory. To express these facts we make a special formalized language. When the collection grows we add some inference rules and thus some axioms to compress the knowledge. The next step is to generalize these rules to all expressions in the formalized language. For these rules we introduce some conclusion procedure. In such a way we make small theories for restricted fields of the knowledge. The most important procedure is the mixing of these partial knowledge systems. In that step we glue the theories together and eliminate the contradictions. The last operation is the most complicated one and some simplifying procedures are proposed.
Resumo:
The article presents an algorithm for translation the system, described by MSC document into Petri Net modulo strong bisimulation. Obtained net can be later used for determining various systems' properties. Example of correction error in original system with using if described algorithm presented.
Resumo:
* Work is partially supported by the Lithuanian State Science and Studies Foundation.
Resumo:
Abstract.The algorithms for computation of minimal supported set of solutions for systems of linear Diophantine homogeneous equations over set of natural numbers and basis of systems of linear Diophantine homogeneous and inhomogeneous equations in ring and field of remainders on modulo of a number.
Resumo:
AMS Subj. Classification: 47J10, 47H30, 47H10
Resumo:
Recently Garashuk and Lisonek evaluated Kloosterman sums K (a) modulo 4 over a finite field F3m in the case of even K (a). They posed it as an open problem to characterize elements a in F3m for which K (a) ≡ 1 (mod4) and K (a) ≡ 3 (mod4). In this paper, we will give an answer to this problem. The result allows us to count the number of elements a in F3m belonging to each of these two classes.