Wyniki wyszukiwania - BazTech

1

A Resolution Calculus for First-order Schemata

Aravantinos V., Echenim M., Peltier N.

Fundamenta Informaticae

|

2013

|

Vol. 125, nr 2

101--133

EN

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.

2

On Inferences of Full First-Order Hierarchical Decompositions

Link S.

Fundamenta Informaticae

|

2011

|

Vol. 106, nr 2-4

233-258

EN

Database design aims to find a database schema that permits the efficient processing of common types of queries and updates on future database instances. Full first-order hierarchical decompositions constitute a large class of database constraints that can provide assistance to the database designer in identifying a suitable database schema. We establish finite axiomatisations of full first-order hierarchical decompositions that mimic best database design practice. That is, an inference engine derives all the independent collections of the universal schema during database normalization, and the designer determines during database denormalization which re-combinations of these independent collections manifest the final database schema. We also show that well-known correspondences between multivalued dependencies, degenerated multivalued dependencies, and a fragment of Boolean propositional logic do not extend beyond binary full first-order hierarchical decompositions.

3

Valuation graphs for propositional logic

Stępień L.

Scientific Issues of Jan Długosz University in Częstochowa. Mathematics

|

2010

|

Vol. 15

139--148

EN

In this paper we present the proof system, called the valuation graphs system, which is a new version of two proof procedures: Davis-Putnam and Stålmarck. The novelty is that in the rules we note which propositional variable occurring in some propositional formula does not determine the logical value of that formula. Due to Stålmarck, we define a notion of proof width, corresponding to the width of structure of valuation graph which is a number of applications of dilemma rule. The dilemma rule considers two cases, so the time of proof grows up exponentially.

4

Asymptotic Properties of Logics

Zaionc M.

Schedae Informaticae

|

2003

|

Vol. 12

129-138

EN

This paper presents the number of results concerning problems of asymptotic densities in the variety of propositional logics. We investigate, for propositional formulas, the proportion of tautologies of the given length n against the number of all formulas of length n. We are specially interested in asymptotic behavior of this fraction. We show what the relation between a number of premises of an implicational formula and asymptotic probability of finding a formula with this number of premises is. Furthermore we investigate the distribution of this asymptotic probabilities. Distribution for all formulas is contrasted with the same distribution for tautologies only.

5

Dowody metodą tableaux

Szyper L.

Scientific Issues of Jan Długosz University in Częstochowa. Mathematics

|

1999

|

Vol. 6

107--115