Page 1 Next
M. Eytan (1974)
Mathématiques et Sciences Humaines
On se propose de donner une interprétation algébrique (en calcul des propositions classiques) des notions d'arbres, d'ensembles de Hintikka, de la méthode des tableaux de Beth-Hintikka Smullyan.
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...
Roland Coghetto, Adam Grabowski (2016)
Formalized Mathematics
In our earlier article [12], the first part of axioms of geometry proposed by Alfred Tarski [14] was formally introduced by means of Mizar proof assistant [9]. We defined a structure TarskiPlane with the following predicates: of betweenness between (a ternary relation), of congruence of segments equiv (quarternary relation), which satisfy the following properties: congruence symmetry (A1), congruence equivalence relation (A2), congruence identity (A3), segment construction (A4), SAS (A5), betweenness...
Kharlampovich, Olga, Myasnikov, Alexei (1998)
Electronic Research Announcements of the American Mathematical Society [electronic only]
Flavio Previale (1975)
Rendiconti del Seminario Matematico della Università di Padova
Stefano Aguzzoli (2000)
Bollettino dell'Unione Matematica Italiana
Esko Turunen (1992)
Kybernetika
Santocanale, Luigi (2001)
Theory and Applications of Categories [electronic only]
Mariusz Giero (2011)
Formalized Mathematics
The article introduces propositional linear time temporal logic as a formal system. Axioms and rules of derivation are defined. Soundness Theorem and Deduction Theorem are proved [9].
Mariusz Giero (2016)
Formalized Mathematics
This article introduces propositional logic as a formal system ([14], [10], [11]). The formulae of the language are as follows φ ::= ⊥ | p | φ → φ. Other connectives are introduced as abbrevations. The notions of model and satisfaction in model are defined. The axioms are all the formulae of the following schemes α ⇒ (β ⇒ α), (α ⇒ (β ⇒ γ)) ⇒ ((α ⇒ β) ⇒ (α ⇒ γ)), (¬β ⇒ ¬α) ⇒ ((¬β ⇒ α) ⇒ β). Modus ponens is the only derivation rule. The soundness theorem and the strong completeness theorem are proved....
Kazuhisa Nakasho, Keiko Narita, Yasunari Shidama (2016)
Formalized Mathematics
In this article, the basic existence theorem of Riemann-Stieltjes integral is formalized. This theorem states that if f is a continuous function and ρ is a function of bounded variation in a closed interval of real line, f is Riemann-Stieltjes integrable with respect to ρ. In the first section, basic properties of real finite sequences are formalized as preliminaries. In the second section, we formalized the existence theorem of the Riemann-Stieltjes integral. These formalizations are based on [15],...
Herrmann, Robert A. (2004)
International Journal of Mathematics and Mathematical Sciences
Jaroslav Janák (1984)
Kybernetika
Hines, Peter (1999)
Theory and Applications of Categories [electronic only]
Motti Abramsky (1980)
Archiv für mathematische Logik und Grundlagenforschung
Itala M.L. D'Ottaviano (1985)
Revista colombiana de matematicas
Tomáš Havránek (1974)
Kybernetika
W.N. Reinhardt (1985)
Revista colombiana de matematicas
James H. Schmerl (1976)
Colloquium Mathematicae
Mariusz Giero (2012)
Formalized Mathematics
This is a preliminary article to prove the completeness theorem of an extension of basic propositional temporal logic. We base it on the proof of completeness for basic propositional temporal logic given in [12]. We introduce n-ary connectives and prove their properties. We derive temporal logic formulas.
Page 1 Next