Inhaltsverzeichnis
Auswahl der wissenschaftlichen Literatur zum Thema „Dedukti“
Geben Sie eine Quelle nach APA, MLA, Chicago, Harvard und anderen Zitierweisen an
Machen Sie sich mit den Listen der aktuellen Artikel, Bücher, Dissertationen, Berichten und anderer wissenschaftlichen Quellen zum Thema "Dedukti" bekannt.
Neben jedem Werk im Literaturverzeichnis ist die Option "Zur Bibliographie hinzufügen" verfügbar. Nutzen Sie sie, wird Ihre bibliographische Angabe des gewählten Werkes nach der nötigen Zitierweise (APA, MLA, Harvard, Chicago, Vancouver usw.) automatisch gestaltet.
Sie können auch den vollen Text der wissenschaftlichen Publikation im PDF-Format herunterladen und eine Online-Annotation der Arbeit lesen, wenn die relevanten Parameter in den Metadaten verfügbar sind.
Zeitschriftenartikel zum Thema "Dedukti"
Assaf, Ali, und Guillaume Burel. „Translating HOL to Dedukti“. Electronic Proceedings in Theoretical Computer Science 186 (30.07.2015): 74–88. http://dx.doi.org/10.4204/eptcs.186.8.
Der volle Inhalt der QuelleCauderlier, Raphaël, und Pierre Halmagrand. „Checking Zenon Modulo Proofs in Dedukti“. Electronic Proceedings in Theoretical Computer Science 186 (30.07.2015): 57–73. http://dx.doi.org/10.4204/eptcs.186.7.
Der volle Inhalt der QuelleAssaf, Ali, und Raphaël Cauderlier. „Mixing HOL and Coq in Dedukti (Extended Abstract)“. Electronic Proceedings in Theoretical Computer Science 186 (30.07.2015): 89–96. http://dx.doi.org/10.4204/eptcs.186.9.
Der volle Inhalt der QuelleEl Haddad, Mohamed Yacine, Guillaume Burel und Frédéric Blanqui. „EKSTRAKTO A tool to reconstruct Dedukti proofs from TSTP files (extended abstract)“. Electronic Proceedings in Theoretical Computer Science 301 (23.08.2019): 27–35. http://dx.doi.org/10.4204/eptcs.301.5.
Der volle Inhalt der QuelleBarras, Bruno, und Valentin Maestracci. „Implementation of Two Layers Type Theory in Dedukti and Application to Cubical Type Theory“. Electronic Proceedings in Theoretical Computer Science 332 (12.01.2021): 54–67. http://dx.doi.org/10.4204/eptcs.332.4.
Der volle Inhalt der QuelleBarras, Bruno, und Valentin Maestracci. „Implementation of Two Layers Type Theory in Dedukti and Application to Cubical Type Theory“. Electronic Proceedings in Theoretical Computer Science 332 (12.01.2021): 54–67. http://dx.doi.org/10.4204/eptcs.332.4.
Der volle Inhalt der QuelleFebriyani, Komang Ayu Dita. „Perspektif Sah Global tentang Serangan Militer AS Lakukan Di Wilayah Irak dan Suriah“. Jurnal Ilmu Hukum Sui Generis 2, Nr. 1 (01.11.2021): 31–45. http://dx.doi.org/10.23887/jih.v2i1.1010.
Der volle Inhalt der QuelleBry, François, und Dietmar Seipel. „Deduktive Datenbanken“. Informatik-Spektrum 19, Nr. 4 (23.08.1996): 214–15. http://dx.doi.org/10.1007/s002870050033.
Der volle Inhalt der QuelleFadillah, Ahmad. „Analisis Kemampuan Penalaran Deduktif Matematis Siswa“. JTAM | Jurnal Teori dan Aplikasi Matematika 3, Nr. 1 (01.04.2019): 15. http://dx.doi.org/10.31764/jtam.v3i1.752.
Der volle Inhalt der QuelleHammer, Martin. „Deduktion und Dialektik“. Hegel-Jahrbuch 2016, Nr. 1 (01.05.2016): 387–93. http://dx.doi.org/10.1515/hgjb-2016-0165.
Der volle Inhalt der QuelleDissertationen zum Thema "Dedukti"
Thiré, François. „Interoperability between proof systems using the logical framework Dedukti“. Electronic Thesis or Diss., université Paris-Saclay, 2020. http://www.theses.fr/2020UPASG053.
Der volle Inhalt der QuelleThere is today a large family of proof systems based upon variouslogics: The Calculus of Inductive Constructions, Higher-Order logic orSet theory, etc. The diversity of proof systems has the negativeconsequence that theorems are formalized many times. One way toovercome this issue would be to make proof systems interoperable. Inthis thesis, we have tackled the interoperability problem for proofsystems both on the theoretical and the practical side using theDedukti logical framework.We begin our journey by looking at Cumulative Type Systems (CTS), afamily of type systems which extends that of Pure Type Systemswith a subtyping relation. CTS provides a common skeleton to manylogics used today. The logic behind Coq, HOL-Light, Lean, Matita orPVS can be seen as an extension of CTS with various features(inductive types, proof irrelevance, predicate subtyping, …). Wedefine a new notion of embedding between CTS. We also provide a soundbut incomplete algorithm to decide whether a proof in one CTS can betranslated into another CTS. This algorithm can also be seen as anextension of Coq's algorithm to check that the floating universeconstraints are consistent. Then, we propose a new embedding of CTSinto Dedukti and give a soundness proof of this embedding. Theseresults show that Dedukti is suitable for studying interoperability onthe theoretical side.We continue our journey on a case of study: The proof of Fermat'slittle theorem written in Matita. We show how we were able totranslate this proof to various proof systems through Dedukti. Thistranslation mainly relies on two tools created for this purpose:— Dkmeta, a tool which proposes to use rewriting as a way to writeproofs transformation programs. One advantage of this tool is that itreuses the syntax of Dedukti itself.— Universo, a tool which implements the aforementioned algorithm whichallows to translate a proof in one CTS (written in Dedukti) toanother.This semi-automatic translation allows to translate the proof ofFermat's little theorem into a weak but expressive logic calledSTTforall. STTforall is a constructive version of Simple Type Theorywith prenex polymorphism. As a consequence, a proof in STTforall canbe exported easily to many proof systems. This case of study showsthat Dedukti is also suitable for interoperability on the practicalside.The tools used for these transformations could be reused also forproofs coming from other proof systems for which an encoding inDedukti is known (such as Coq or Agda).The journey ends with the exportation of the proof of Fermat's littletheorem encoded in STTforall towards 5 different proof systems: Coq,Lean, Matita, OpenTheory (a member of the HOL-family proof systems)and PVS. We have implemented a user interface for that via a websitecalled Logipedia.Logipedia was designed with the goal of containing many more proofs thatcould be shared between proof systems and as such is intended to be anencyclopedia of formal proofs
Hondet, Gabriel. „Expressing predicate subtyping in computational logical frameworks“. Electronic Thesis or Diss., université Paris-Saclay, 2022. http://www.theses.fr/2022UPASG070.
Der volle Inhalt der QuelleSafe programming as well as most proof systems rely on typing. The more a type system is expressive, the more these types can be used to encode invariants which are therefore verified mechanically through type checking procedures. Dependent types extend simple types by allowing types to depend on values. For instance, it allows to define the types of lists of a certain length. Predicate subtyping is another extension of simple type theory in which types can be defined by predicates. A predicate subtype, usually noted {x: A | P(x)}, is inhabited by elements t of type A for which P(t) is true. This extension provides an extremely rich and intuitive type system, which is at the heart of the proof assistant PVS, at the cost of making type checking undecidable.This work is dedicated to the encoding of predicate subtyping in Dedukti: a logical framework with computation rules. We begin with the encoding of explicit predicate subtyping for which the terms in {x: A | P(x)} and terms of Aare syntactically different. We show that any derivable judgement of predicate subtyping can be encoded into a derivable judgement of the logical framework. Predicate subtyping, is often used implicitly: with no syntactic difference between terms of type A and terms of type {x: A | P(x) }. We enrich our logical framework with a term refiner which can add these syntactic markers. This refiner can be used to refine judgements typed with implicit predicate subtyping into explicited judgements.The proof assistant PVS uses extensively predicate subtyping. We show how its standard library can be exported to Dedukti. Because PVS only store proof traces rather than complete proof terms, we sketch in the penultimate section a procedure to generate complete proof terms from these proof traces.The last section provides the architecture of a repository dedicated to the exchange of formal proofs. The goal of such a repository is to categorise and store proofs encoded in Dedukti to promote interoperability
Schiefele, Ulrich, und Klaus Peter Wild. „Induktiv versus deduktiv entwickelte Fragebogenverfahren zur Erfassung von Merkmalen des Lernverhaltens“. Universität Potsdam, 1993. http://opus.kobv.de/ubp/volltexte/2009/3359/.
Der volle Inhalt der QuelleCurrently available questionnaires to measure strategies, styles, and orientations of learning seem to fall in two different groups. The first group employed an inductive procedure and proposed relatively global learner characteristics that were derived from interview studies. These characteristics typically involve motivational as well as cognitive components. The second group of measures did proceed deductively. On the basis of cognitive models of the learning process and theories of motivation, questionnaires were developed with rather specific subscales of learning strategies and motivational characteristics. These measures, however, have strictly separated cognitive and motivational components of learning. In the present article, we selected two representative examples of each group of questionnaires and discussed their advantages and disadvantages.
Lindner, Philip. „Det där är ingen icke-zebra! : epistemisk-deduktiv slutenhet och skepticism“. Thesis, Umeå universitet, Institutionen för idé- och samhällsstudier, 2011. http://urn.kb.se/resolve?urn=urn:nbn:se:umu:diva-52691.
Der volle Inhalt der QuelleJönsson, Joakim, und Pontus Strandell. „Motivation för förändring : En deduktiv forskning baserad på den transteoretiska modellen“. Thesis, Karlstads universitet, Fakulteten för samhälls- och livsvetenskaper, 2014. http://urn.kb.se/resolve?urn=urn:nbn:se:kau:diva-32635.
Der volle Inhalt der QuelleThe purpose of this research was to examine and understand how a process of change with a connection to motivation looks like. The individuals of which participated in the study had a common factor of changing their lifestyle after living with a fatal or potentially fatal behavior. With an attachment to the transtheoretical model we have examined whether the respondents have followed through the levels of readiness in the model in their process towards a healthier behavior pattern. By using an open dialog in the interviews we were able to examine the depth in the statements of the respondents. The final results showed among others that the inner motivation of which is experienced is essential in the maintenance of the new behavior, and that the solidarity in the various support groups of which the respondents had participated was crucial to their outer motivation.
Mickelsson, Johanna, und Anna-Liv Sollerman. „Betydelsen av KASAM hos personer som genom gått enhjärtinfarkt. : ‑ En deduktiv litteraturöversikt“. Thesis, Mittuniversitetet, Avdelningen för omvårdnad, 2018. http://urn.kb.se/resolve?urn=urn:nbn:se:miun:diva-33874.
Der volle Inhalt der QuelleGodkännande datum: 2018-03-28
Сорочан, Д. В. „Переваги використання Deduktor при аналізі лояльності покупців“. Thesis, ТОВ «ДД «Папірус», 2013. http://essuir.sumdu.edu.ua/handle/123456789/37548.
Der volle Inhalt der QuelleKaleja, Bernadette. „Den deduktiva grammatikundervisningens inverkan på tyskelevers interlanguage“. Thesis, Malmö högskola, Lärarutbildningen (LUT), 2008. http://urn.kb.se/resolve?urn=urn:nbn:se:mau:diva-35021.
Der volle Inhalt der QuelleThis degree project is based on four questions and one hypothesis about the effects of deductive grammar instruction on the interlanguage of pupils who are learning German. The study attempts to show whether the deductive method favours a certain group of pupils due to ethnicity and gender. The study consists of a Grammaticality Judgement Test and a set of interviews conducted on pupils who are learning German as their optional choice of a foreign language in the upper primary school years 8 and 9. The grammatical structures that the pupils are tested on were taught spring term 2008 in connection with the regular German language lessons. By assuming that some kind of learning has occurred, the pupils were asked to explain how it took place. The results show that the deductive grammar instruction appears to favour girls with Swedish background as well as girls with a foreign background.
Algulin, David, und Jesper Sandberg. „Induktiva och deduktiva arbetssätt inom matematik : En systematisk litteraturstudie om hur induktiva och deduktiva arbetssätt kan påverka elevers matematiska förståelse“. Thesis, Linnéuniversitetet, Institutionen för matematik (MA), 2021. http://urn.kb.se/resolve?urn=urn:nbn:se:lnu:diva-101069.
Der volle Inhalt der QuelleKoc, Bobil. „Induktiv och deduktiv konkretisering i praktiken : En studie i årskurs 1-3 om hur induktiv och deduktiv konkretisering som didaktisk metod i matematikundervisning kan främja ett utvecklande av kunskap och lärande“. Thesis, Södertörns högskola, Lärarutbildningen, 2017. http://urn.kb.se/resolve?urn=urn:nbn:se:sh:diva-34276.
Der volle Inhalt der QuelleBücher zum Thema "Dedukti"
Cremers, Armin B., Ulrike Griefahn und Ralf Hinze. Deduktive Datenbanken. Wiesbaden: Vieweg+Teubner Verlag, 1994. http://dx.doi.org/10.1007/978-3-663-09572-9.
Der volle Inhalt der QuelleDeduct It! Berkeley: NOLO, 2007.
Den vollen Inhalt der Quelle findenBüning, Hans Kleine, und Theodor Lettmann. Aussagenlogik: Deduktion und Algorithmen. Wiesbaden: Vieweg+Teubner Verlag, 1994. http://dx.doi.org/10.1007/978-3-322-84809-3.
Der volle Inhalt der QuelleBüning, H. Kleine. Aussagenlogik: Deduktion und Algorithmen. Stuttgart: B.G. Teubner, 1994.
Den vollen Inhalt der Quelle findenArifin, Syamsul. Pengembangan paragraf deduktif dalam media massa cetak berbahasa Jawa. Yogyakarta: Kementerian Pendidikan Nasional, Pusat Bahasa, Balai Bahasa Yogyakarta, 2010.
Den vollen Inhalt der Quelle findenUnited States. Internal Revenue Service. How to deduct backup withholding. [Washington, D.C.?: Dept. of the Treasury, Internal Revenue Service, 1994.
Den vollen Inhalt der Quelle findenPietrini, Stefania. Deducto usu fructu: Una nuova ipotesi sull'origine dell'usufrutto. Milano: A. Giuffrè, 2008.
Den vollen Inhalt der Quelle findenForum für Philosophie Bad Homburg., Hrsg. Kants transzendentale Deduktion und die Möglichkeit von Transzendentalphilosophie. Frankfurt am Main: Suhrkamp, 1988.
Den vollen Inhalt der Quelle findenSchönecker, Dieter. Kant--Grundlegung III: Die Deduktion des kategorischen Imperativs. Freiburg: Alber, 1999.
Den vollen Inhalt der Quelle findenDeduct it!: Lower your small business taxes. 5. Aufl. Berkeley, Calif: Nolo, 2008.
Den vollen Inhalt der Quelle findenBuchteile zum Thema "Dedukti"
Cauderlier, Raphaël. „Tactics and Certificates in Meta Dedukti“. In Interactive Theorem Proving, 142–59. Cham: Springer International Publishing, 2018. http://dx.doi.org/10.1007/978-3-319-94821-8_9.
Der volle Inhalt der QuelleCauderlier, Raphaël, und Catherine Dubois. „FoCaLiZe and Dedukti to the Rescue for Proof Interoperability“. In Interactive Theorem Proving, 131–47. Cham: Springer International Publishing, 2017. http://dx.doi.org/10.1007/978-3-319-66107-0_9.
Der volle Inhalt der QuelleCauderlier, Raphaël, und Catherine Dubois. „ML Pattern-Matching, Recursion, and Rewriting: From FoCaLiZe to Dedukti“. In Theoretical Aspects of Computing – ICTAC 2016, 459–68. Cham: Springer International Publishing, 2016. http://dx.doi.org/10.1007/978-3-319-46750-4_26.
Der volle Inhalt der QuelleAltenbach, Holm. „Deduktiv abgeleitete Materialgleichungen“. In Kontinuumsmechanik, 231–52. Berlin, Heidelberg: Springer Berlin Heidelberg, 2015. http://dx.doi.org/10.1007/978-3-662-47070-1_7.
Der volle Inhalt der QuelleAltenbach, Holm. „Deduktiv abgeleitete Materialgleichungen“. In Kontinuumsmechanik, 233–54. Berlin, Heidelberg: Springer Berlin Heidelberg, 2012. http://dx.doi.org/10.1007/978-3-642-24119-2_7.
Der volle Inhalt der QuelleAltenbach, Holm. „Deduktiv abgeleitete Konstitutivgleichungen“. In Kontinuumsmechanik, 233–54. Berlin, Heidelberg: Springer Berlin Heidelberg, 2018. http://dx.doi.org/10.1007/978-3-662-57504-8_7.
Der volle Inhalt der QuelleCremers, Armin B., Ulrike Griefahn und Ralf Hinze. „Einleitung“. In Deduktive Datenbanken, 1–16. Wiesbaden: Vieweg+Teubner Verlag, 1994. http://dx.doi.org/10.1007/978-3-663-09572-9_1.
Der volle Inhalt der QuelleCremers, Armin B., Ulrike Griefahn und Ralf Hinze. „Prädikatenlogik“. In Deduktive Datenbanken, 17–51. Wiesbaden: Vieweg+Teubner Verlag, 1994. http://dx.doi.org/10.1007/978-3-663-09572-9_2.
Der volle Inhalt der QuelleCremers, Armin B., Ulrike Griefahn und Ralf Hinze. „Deduktive Datenbanken“. In Deduktive Datenbanken, 53–110. Wiesbaden: Vieweg+Teubner Verlag, 1994. http://dx.doi.org/10.1007/978-3-663-09572-9_3.
Der volle Inhalt der QuelleCremers, Armin B., Ulrike Griefahn und Ralf Hinze. „Alternative Auswertungsmethoden“. In Deduktive Datenbanken, 111–45. Wiesbaden: Vieweg+Teubner Verlag, 1994. http://dx.doi.org/10.1007/978-3-663-09572-9_4.
Der volle Inhalt der QuelleKonferenzberichte zum Thema "Dedukti"
Gharaibeh, Abdullah, Cornel Constantinescu, Maohua Lu, Ramani Routray, Anurag Sharma, Prasenjit Sarkar, David Pease und Matei Ripeanu. „DedupT: Deduplication for tape systems“. In 2014 30th Symposium on Mass Storage Systems and Technologies (MSST). IEEE, 2014. http://dx.doi.org/10.1109/msst.2014.6855555.
Der volle Inhalt der QuelleOrwant, Jon, und Walter R. Bender. „Color Deducto: playing games to learn about color“. In Electronic Imaging, herausgegeben von Bernice E. Rogowitz und Thrasyvoulos N. Pappas. SPIE, 2000. http://dx.doi.org/10.1117/12.387210.
Der volle Inhalt der QuelleFornaia, Andrea, und Emiliano Tramontana. „DeDuCT: A Data Dependence Based Concern Tagger for Modularity Analysis“. In 2017 IEEE 41st Annual Computer Software and Applications Conference (COMPSAC). IEEE, 2017. http://dx.doi.org/10.1109/compsac.2017.98.
Der volle Inhalt der QuelleMardianis. „Integrasi Kemampuan Negara-Negara dalam Penerbangan dan Antariksa“. In Seminar Nasional Kebijakan Penerbangan dan Antariksa I. Bogor: In Media, 2017. http://dx.doi.org/10.30536/p.sinaskpa.i.5.
Der volle Inhalt der QuelleWang, Hui, und Pu Zhang. „Online Intelligent Monitoring System for Operation States of Dedust Facilities in a Steel Plant“. In 2019 International Conference on Artificial Intelligence and Advanced Manufacturing (AIAM). IEEE, 2019. http://dx.doi.org/10.1109/aiam48774.2019.00159.
Der volle Inhalt der QuelleDhirgawati, Mutia, Lusiyana Alvionita Simbolon, Dyan Cynthia Anggraini und Naniek Widayati Priyomarsono. „Usulan Kriteria Konservasi pada Pura Pajinengan Gunung Tap Sai Kabupaten Karangasem – Bali sebagai Warisan Budaya“. In Temu Ilmiah IPLBI 2021. Ikatan Peneliti Lingkungan Binaan Indonesia, 2021. http://dx.doi.org/10.32315/ti.9.k115.
Der volle Inhalt der QuelleGu, Li-ping, Jian-feng Gu und Xiao Yi. „Design of fuzzy controller for flue gas temperature of dedust with self-set correction factor“. In 2011 23rd Chinese Control and Decision Conference (CCDC). IEEE, 2011. http://dx.doi.org/10.1109/ccdc.2011.5968327.
Der volle Inhalt der QuelleHajjaj, Mohammed, Mitsunori Miki und Kitsunori Shimohara. „The Effect of Using the Intelligent Lighting System to Deduct the Power Consumption at the Office“. In 2019 IEEE 7th Conference on Systems, Process and Control (ICSPC). IEEE, 2019. http://dx.doi.org/10.1109/icspc47137.2019.9068078.
Der volle Inhalt der QuelleHrabčák, Ladislav. „Na ceste k digitálnemu euru“. In IV.SLOVENSKO-ČESKÉ DNI DAŇOVÉHO PRÁVA. Univerzita Pavla Jozefa Šafárika, 2021. http://dx.doi.org/10.33542/scd21-0043-1-11.
Der volle Inhalt der QuelleMo, Shixiu, und Lingyun Kong. „A study on the determination method of the rut deduct value in the calculation of asphalt pavement condition index“. In 2011 International Conference on Electric Technology and Civil Engineering (ICETCE). IEEE, 2011. http://dx.doi.org/10.1109/icetce.2011.5774206.
Der volle Inhalt der Quelle