All a b c d e f g h i j k l m n o p q r s t u v w x y z Other

Page 1

Displaying 1 – 12 of 12

Showing per page

Taclets: a new paradigm for constructing interactive theorem provers.

Bernhard Beckert, Martin Giese, Elmar Habermalz, Reiner Hähnle, Andreas Roth, Philipp Rümmer, Steffen Schlager (2004)

RACSAM

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.

Przemyslaw Grzegorzewski, Olgierd Hryniewicz (1997)

Mathware and Soft Computing

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

Julian J. Schlöder, Peter Koepke (2012)

Formalized Mathematics

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.

Towards the automated synthesis of a Gröbner bases algorithm.

Bruno Buchberger (2004)

RACSAM

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

Julian J. Schlöder, Peter Koepke (2012)

Formalized Mathematics

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.

Currently displaying 1 – 12 of 12

Page 1