Fundamenta Informaticae - Volume 125, issue 2

Authors: Aravantinos, Vincent | Echenim, Mnacho | Peltier, Nicolas

Article Type: Research Article

Abstract: We devise a resolution calculus that tests the satisfiability of infinite families of clause sets, called clause set schemata. For schemata of propositional clause sets, we prove that this calculus is sound, refutationally complete, and terminating. The calculus is extended to first-order clauses, for which termination is lost, since the satisfiability problem is not semi-decidable for nonpropositional schemata. The expressive power of the considered logic is strictly greater than the one considered in our previous work.

Keywords: Propositional logic, first-order logic, schemata, resolution calculus

DOI: 10.3233/FI-2013-855

Citation: Fundamenta Informaticae, vol. 125, no. 2, pp. 101-133, 2013

Authors: Dong, Jianwu | Chen, Feng | Huo, Yanyan | Liu, Hong

Article Type: Research Article

Abstract: This paper proposes a new method, conditional probability table (CPT) decomposition, to analyze the independent and deterministic components of CPT. This method can be used to approximate and analyze Baysian networks. The decomposition of Bayesian networks is accomplished by representing CPTs as a linear combination of extreme CPTs, which forms a new framework to conduct inference. Based on this new framework, inference in Bayesian networks can be done by decomposing them into less connected and weighted subnetworks. We can achieve exact inference if the original network is decomposed into singly-connected subnetworks. Besides, approximate inference can be done by discarding the …subnetworks with small weights or by a partial decomposition and application of belief propagation (BP) on the still multiply-connected subnetworks. Experiments show that the decomposition-based approximation outperforms BP in most cases. Show more

Keywords: Bayesian network, conditional probability table, inference, decomposition

DOI: 10.3233/FI-2013-856

Citation: Fundamenta Informaticae, vol. 125, no. 2, pp. 135-152, 2013

Authors: Erveš, Rija | Žerovnik, Janez

Article Type: Research Article

Abstract: The product graph B * F of graphs B and F is an interesting model in the design of large reliable networks. Fault tolerance and transmission delay of networks are important concepts in network design. The notions are strongly related to connectivity and diameter of a graph, and have been studied by many authors. Wide diameter of a graph combines studying connectivity with the diameter of a graph. Diameter with width k of a graph G, k-diameter, is defined as the minimum integer d for which there exist at least k internally disjoint paths of length at most d between …any two distinct vertices in G. Denote by $\cal{D}^W_c (G)$ the c-diameter of G and κ(G) the connectivity of G. We prove that $\cal{D}^W_{a+b}(B * F) \le r_a(F) + \cal{D}^W_b (B) + 1$ for a ≤ κ(F) and b ≤ κ(B). The Rabin number rc (G) is the minimum integer d such that there are c internally disjoint paths of length at most d from any vertex v to any set of c vertices {v1 , v2 , ... , vc }. Show more

Keywords: product graph, Wide-diameter, Rabin number, fault diameter, Cartesian graph bundle

DOI: 10.3233/FI-2013-857

Citation: Fundamenta Informaticae, vol. 125, no. 2, pp. 153-160, 2013

Authors: Grześkowiak, Maciej

Article Type: Research Article

Abstract: We present a general method of generating primes p and q such that q divides Φn (p), where n > 2 is a fixed number. In particular, we present the deterministic method of finding a primitive nth roots of unity modulo q. We estimate the computational complexity of our methods.

Keywords: primes of a special form, computing a primitive nth root of unity modulo primes, public key cryptography

DOI: 10.3233/FI-2013-858

Citation: Fundamenta Informaticae, vol. 125, no. 2, pp. 161-181, 2013

Authors: Kosiuczenko, Piotr

Article Type: Research Article

Abstract: The paradigm of contractual specification provides a transparent way of specifying object-oriented systems. In this paradigm, system consistency is specified using so-called invariants. Runtime validation of invariants is a complex problem. Existing validation methods require either exhausting validation of an invariant for all objects of the corresponding class or the use of restrictive type systems. In this paper a non-exhaustive method of invariant validation is proposed. It is proved that the method is sound and an implementation of this method is discussed. It is shown also how to extract context free languages corresponding to OCL-invariants.

Keywords: OCL, contracts, invariant validation, framing, optimization

DOI: 10.3233/FI-2013-859

Citation: Fundamenta Informaticae, vol. 125, no. 2, pp. 183-222, 2013