Statistical deducibility testing with stochastic parameters
Statistical methods for comparing theorem proving algorithms
Statistical testing procedure for lengths of formalized proofs
Statistical theory of logical derivability
Taclets: a new paradigm for constructing interactive theorem provers.
Frameworks for interactive theorem proving give the user explicit control over the construction of proofs based on meta languages that contain dedicated control structures for describing proof construction. Such languages are not easy to master and thus contribute to the already long list of skills required by prospective users of interactive theorem provers. Most users, however, only need a convenient formalism that allows to introduce new rules with minimal overhead. On the the other hand, rules...
Testing statistical hypotheses in fuzzy environment.
In traditional statistics all parameters of the mathematical model and possible observations should be well defined. Sometimes such assumption appears too rigid for the real-life problems, especially while dealing with linguistic data or imprecise requirements. To relax this rigidity fuzzy methods are incorporated into statistics. We review hitherto existing achievements in testing statistical hypotheses in fuzzy environment, point out their advantages or disadvantages and practical problems. We...
The Gödel Completeness Theorem for Uncountable Languages
This article is the second in a series of two Mizar articles constituting a formal proof of the Gödel Completeness theorem [15] for uncountably large languages. We follow the proof given in [16]. The present article contains the techniques required to expand a theory such that the expanded theory contains witnesses and is negation faithful. Then the completeness theorem follows immediately.
The GUHA method and the three-valued logic
The statistical interpretation and modification of GUHA method
Theorem Provers for Substructural Logics
Theorem proving through depth-first test
Theorem-proving systems [Book]
Three semantical interpretations of a statistical theoremhood testing procedure
Towards automated proofs of observational properties.
Towards the automated synthesis of a Gröbner bases algorithm.
We discuss the question of whether the central result of algorithmic Gröbner bases theory, namely the notion of S?polynomials together with the algorithm for constructing Gröbner bases using S?polynomials, can be obtained by ?artificial intelligence?, i.e. a systematic (algorithmic) algorithm synthesis method. We present the ?lazy thinking? method for theorem and algorithm invention and apply it to the ?critical pair / completion? algorithm scheme. We present a road map that demonstrates that, with...
Transition of Consistency and Satisfiability under Language Extensions
This article is the first in a series of two Mizar articles constituting a formal proof of the Gödel Completeness theorem [17] for uncountably large languages. We follow the proof given in [18]. The present article contains the techniques required to expand formal languages. We prove that consistent or satisfiable theories retain these properties under changes to the language they are formulated in.
Unification in varieties of idempotent semigroups.
Uniqueness of Steiner laws on cubic curves.
Using automated reasoning tools: A study of the semigroup F2B2.
Veblen Hierarchy
The Veblen hierarchy is an extension of the construction of epsilon numbers (fixpoints of the exponential map: ωε = ε). It is a collection φα of the Veblen Functions where φ0(β) = ωβ and φ1(β) = εβ. The sequence of fixpoints of φ1 function form φ2, etc. For a limit non empty ordinal λ the function φλ is the sequence of common fixpoints of all functions φα where α < λ.The Mizar formalization of the concept cannot be done directly as the Veblen functions are classes (not (small) sets). It is done...