Gotowe bibliografie tematyczne / Proof reconstruction

Gotowa bibliografia na temat „Proof reconstruction”

Autor: Grafiati

Data publikacji: 25 maja 2024

Utwórz poprawne odniesienie w stylach APA, MLA, Chicago, Harvard i wielu innych

Wybierz rodzaj źródła:

Spis treści

Artykuły w czasopismach
Rozprawy doktorskie
Książki
Części książek
Streszczenia konferencji
Raporty organizacyjne

Zobacz listy aktualnych artykułów, książek, rozpraw, streszczeń i innych źródeł naukowych na temat „Proof reconstruction”.

Przycisk „Dodaj do bibliografii” jest dostępny obok każdej pracy w bibliografii. Użyj go – a my automatycznie utworzymy odniesienie bibliograficzne do wybranej pracy w stylu cytowania, którego potrzebujesz: APA, MLA, Harvard, Chicago, Vancouver itp.

Możesz również pobrać pełny tekst publikacji naukowej w formacie „.pdf” i przeczytać adnotację do pracy online, jeśli odpowiednie parametry są dostępne w metadanych.

Artykuły w czasopismach na temat "Proof reconstruction"

Bundy, Alan, Mateja Jamnik i Andrew Fugard. "What is a proof?" Philosophical Transactions of the Royal Society A: Mathematical, Physical and Engineering Sciences 363, nr 1835 (14.09.2005): 2377–91. http://dx.doi.org/10.1098/rsta.2005.1651.

Pełny tekst źródła

Streszczenie:

To those brought up in a logic-based tradition there seems to be a simple and clear definition of proof. But this is largely a twentieth century invention; many earlier proofs had a different nature. We will look particularly at the faulty proof of Euler's Theorem and Lakatos' rational reconstruction of the history of this proof. We will ask: how is it possible for the errors in a faulty proof to remain undetected for several years—even when counter-examples to it are known? How is it possible to have a proof about concepts that are only partially defined? And can we give a logic-based account of such phenomena? We introduce the concept of schematic proofs and argue that they offer a possible cognitive model for the human construction of proofs in mathematics. In particular, we show how they can account for persistent errors in proofs.

Style APA, Harvard, Vancouver, ISO itp.

Francez, Nissim, i Gilad Ben-Avi. "Proof-Theoretic Reconstruction of Generalized Quantifiers". Journal of Semantics 32, nr 3 (20.03.2014): 313–71. http://dx.doi.org/10.1093/jos/ffu001.

Pełny tekst źródła

Style APA, Harvard, Vancouver, ISO itp.

Fasan, Oluwasola Mary, i Martin S. Olivier. "Correctness proof for database reconstruction algorithm". Digital Investigation 9, nr 2 (listopad 2012): 138–50. http://dx.doi.org/10.1016/j.diin.2012.09.002.

Pełny tekst źródła

Style APA, Harvard, Vancouver, ISO itp.

Iványi, Antal. "Reconstruction of score sets". Acta Universitatis Sapientiae, Informatica 6, nr 2 (1.12.2014): 210–29. http://dx.doi.org/10.1515/ausi-2015-0005.

Pełny tekst źródła

Streszczenie:

Abstract The score set of a tournament is defined as the set of its different outdegrees. In 1978 Reid [15] published the conjecture that for any set of nonnegative integers D there exists a tournament T whose degree set is D. Reid proved the conjecture for tournaments containing n = 1, 2, and 3 vertices. In 1986 Hager [4] published a constructive proof of the conjecture for n = 4 and 5 vertices. In 1989 Yao [18] presented an arithmetical proof of the conjecture, but general polynomial construction algorithm is not known. In [6] we described polynomial time algorithms which reconstruct the score sets containing only elements less than 7. In [5] we improved this bound to 9. In this paper we present and analyze new algorithms Hole-Map, Hole-Pairs, Hole-Max, Hole-Shift, Fill-All, Prefix-Deletion, and using them improve the above bound to 12, giving a constructive partial proof of Reid’s conjecture.

Style APA, Harvard, Vancouver, ISO itp.

Banach, R. "Sequent reconstruction in LLM—A sweepline proof". Annals of Pure and Applied Logic 73, nr 3 (czerwiec 1995): 277–95. http://dx.doi.org/10.1016/0168-0072(94)00033-y.

Pełny tekst źródła

Style APA, Harvard, Vancouver, ISO itp.

Krajewski, Stanisław. "Anti-foundationalist Philosophy of Mathematics and Mathematical Proofs". Studia Humana 9, nr 3-4 (1.10.2020): 154–64. http://dx.doi.org/10.2478/sh-2020-0034.

Pełny tekst źródła

Streszczenie:

Abstract The Euclidean ideal of mathematics as well as all the foundational schools in the philosophy of mathematics have been contested by the new approach, called the “maverick” trend in the philosophy of mathematics. Several points made by its main representatives are mentioned – from the revisability of actual proofs to the stress on real mathematical practice as opposed to its idealized reconstruction. Main features of real proofs are then mentioned; for example, whether they are convincing, understandable, and/or explanatory. Therefore, the new approach questions Hilbert’s Thesis, according to which a correct mathematical proof is in principle reducible to a formal proof, based on explicit axioms and logic.

Style APA, Harvard, Vancouver, ISO itp.

D’Alpaos, Diana, Giovanni Badiali, Francesco Ceccariglia i Achille Tarsitano. "Delayed Orbital Floor Reconstruction Using Mirroring Technique and Patient-Specific Implants: Proof of Concept". Journal of Personalized Medicine 14, nr 5 (26.04.2024): 459. http://dx.doi.org/10.3390/jpm14050459.

Pełny tekst źródła

Streszczenie:

Enophthalmos is a severe complication of primary reconstruction following orbital floor fractures, oncological resections, or maxillo-facial syndromes. The goal of secondary orbital reconstruction is to regain a symmetrical globe position to restore function and aesthetics. In this article, we present a method of computer-assisted orbital floor reconstruction using a mirroring technique and a custom-made titanium or high-density polyethylene mesh printed using computer-aided manufacturing techniques. This reconstructive protocol involves four steps: mirroring of the healthy orbit computer tomography files at the contralateral affected site, virtual design of a customized implant, computer-assisted manufacturing (CAM) of the implant using Direct Metal Laser Sintering (DMLS) or Computer Numerical Control (CNC) methods, and surgical insertion of the device. Clinical outcomes were assessed using 3dMD photogrammetry and computed tomography measures in 13 treated patients and compared to a control group treated with stock implants. An improvement of 3.04 mm (range 0.3–6 mm) in globe protrusion was obtained for the patients treated with patient-specific implants (PSI), and no major complications have been registered. The technique described here appears to be a viable method for correcting complex orbital floor defects needing delayed reconstruction.

Style APA, Harvard, Vancouver, ISO itp.

RUMBERG, ANTJE. "BOLZANO’S CONCEPT OF GROUNDING (ABFOLGE) AGAINST THE BACKGROUND OF NORMAL PROOFS". Review of Symbolic Logic 6, nr 3 (3.07.2013): 424–59. http://dx.doi.org/10.1017/s1755020313000154.

Pełny tekst źródła

Streszczenie:

AbstractIn this paper, I provide a thorough discussion and reconstruction of Bernard Bolzano’s theory of grounding and a detailed investigation into the parallels between his concept of grounding and current notions of normal proofs. Grounding (Abfolge) is an objective ground-consequence relation among true propositions that is explanatory in nature. The grounding relation plays a crucial role in Bolzano’s proof-theory, and it is essential for his views on the ideal buildup of scientific theories. Occasionally, similarities have been pointed out between Bolzano’s ideas on grounding and cut-free proofs in Gentzen’s sequent calculus. My thesis is, however, that they bear an even stronger resemblance to the normal natural deduction proofs employed in proof-theoretic semantics in the tradition of Dummett and Prawitz.

Style APA, Harvard, Vancouver, ISO itp.

Klima, Gyula. "Aquinas’s Real Distinction and Its Role in a Causal Proof of God’s Existence". Roczniki Filozoficzne 67, nr 4 (23.12.2019): 7–26. http://dx.doi.org/10.18290/rf.2019.67.4-1.

Pełny tekst źródła

Streszczenie:

This paper is not going to offer any criticism of the way Gaven Kerr treats Aquinas’ argument. Instead, it offers an alternative way of reconstructing Aquinas’ argument, intending to strengthen especially those controversial aspects of it that Kerr’s reconstruction left untreated or in relative obscurity. Accordingly, although the paper’s treatment will have to have some overlaps with Kerr’s (such as the critique of Kenny’s critique of Aquinas), it will deal with issues essential to adequate replies to certain competent criticisms of his argument untreated by Kerr (such as Buridan’s critique). For the sake of the “formally inclined” reader, the paper’s treatment will also include an Appendix offering a formal reconstruction of both the main argument and its sub-arguments to demonstrate the formal rigor of Aquinas’ original.

Style APA, Harvard, Vancouver, ISO itp.

Godino-Moya, Alejandro, Rosa-María Menchón-Lara, Marcos Martín-Fernández, Claudia Prieto i Carlos Alberola-López. "Elastic AlignedSENSE for Dynamic MR Reconstruction: A Proof of Concept in Cardiac Cine". Entropy 23, nr 5 (29.04.2021): 555. http://dx.doi.org/10.3390/e23050555.

Pełny tekst źródła

Streszczenie:

Numerous methods in the extensive literature on magnetic resonance imaging (MRI) reconstruction exploit temporal redundancy to accelerate cardiac cine. Some of them include motion compensation, which involves high computational costs and long runtimes. In this work, we proposed a method—elastic alignedSENSE (EAS)—for the direct reconstruction of a motion-free image plus a set of nonrigid deformations to reconstruct a 2D cardiac sequence. The feasibility of the proposed approach was tested in 2D Cartesian and golden radial multi-coil breath-hold cardiac cine acquisitions. The proposed approach was compared against parallel imaging compressed sense (sPICS) and group-wise motion corrected compressed sense (GWCS) reconstructions. EAS provides better results on objective measures with considerable less runtime when an acceleration factor is higher than 10×. Subjective assessment of an expert, however, invited proposing the combination of EAS and GWCS as a preferable alternative to GWCS or EAS in isolation.

Style APA, Harvard, Vancouver, ISO itp.

Więcej źródeł

Rozprawy doktorskie na temat "Proof reconstruction"

El, haddad Yacine. "Integrating Automated Theorem Provers in Proof Assistants". Electronic Thesis or Diss., université Paris-Saclay, 2021. http://www.theses.fr/2021UPASG052.

Pełny tekst źródła

Streszczenie:

Lambdapi est un assistant de preuve qui permet à l’utilisateur la construction d’une preuve d’un théorème donné dans un langage universel basé sur le lambda-pi-calcul. Le but de cette thèse est de rajouter de l’automatisation à Lambdapi pour faire gagner du temps à l’utilisateur. Cette thèse présente trois contributions liées à l’intégration des démonstrateurs automatiques dans les assistants de preuve. La première contribution consiste en l’implémentation d’une tactique qui fait appel au démonstrateurs automatiques depuis Lambdapi à travers une plateforme tiers appelé Why3. Généralement, les démonstrateurs automatiques ne génèrent pas un certificat de preuve complet, d’où la deuxième contribution présentée dans cette thèse: la reconstruction de preuves générées par les démonstrateurs automatiques du premier ordre dans Lambdapi implémenté dans un outil appelé Ekstrakto. Enfin, ces démonstrateurs peuvent parfois effectuer des modifications sur la formule qu'ils sont en train de prouver. Le dernier résultat de la thèse est consacré à la certification des étapes de Skolemisation faites par les démonstrateurs automatiques. Un algorithme est présenté, montré correct et impleménté dans l'outil Skonverto
Lambdapi is a proof assistant that allows users to construct a proof of a given theorem in a universal language based on the lambda-pi-calculus. The goal of this thesis is to add more automation to Lambdapi to gain more time and effort for the users. This thesis presents three contributions associated with the integration of automated provers in proof assistants. The first contribution consists of the implementation of a tactic that calls automated provers from Lambdapi by using an external platform called Why3. Usually, automated provers do not generate a complete certificate of a given formula, thus, the second contribution presented in this thesis is the reconstruction in Lambdapi of proofs generated by first-order automated provers implemented in a tool called Ekstrakto. Finally, automated provers often perform some transformations on the formula that they are trying to solve. Among these transformations, we can find Skolemization steps. The last contribution is devoted to the certification of Skolemization steps performed by the automated provers in order to have a complete reconstruction. This has been implemented in a tool called Skonverto

Style APA, Harvard, Vancouver, ISO itp.

Huang, Xiaorong [Verfasser]. "Human Oriented Proof Presentation: A Reconstructive Approach / Xiaorong Huang". Kaiserslautern : Technische Universität Kaiserslautern, Fachbereich Informatik, 1999. http://d-nb.info/1026735831/34.

Pełny tekst źródła

Style APA, Harvard, Vancouver, ISO itp.

Last, Carsten [Verfasser], i Dr Ing Wahl Friedrich M. [Akademischer Betreuer] Prof. "From Global to Local Statistical Shape Priors - Novel methods to obtain accurate reconstruction results with a limited amount of training shapes / Carsten Last ; Betreuer: Friedrich M. Prof. Dr.-Ing. Wahl". Braunschweig : Technische Universität Braunschweig, 2016. http://d-nb.info/117581816X/34.

Pełny tekst źródła

Style APA, Harvard, Vancouver, ISO itp.

Afonso, Mara Cristina da Conceição. "A reconstituição informática e as provas atípicas em processo penal". Master's thesis, 2017. http://hdl.handle.net/10362/21790.

Pełny tekst źródła

Streszczenie:

This dissertation deals with the theme of atypical evidence in Criminal Procedure in general, and the admissibility of proof by computer reconstruction of the fact, in particular. The general framework of atypical evidence in the portuguese criminal procedure system is fundamental to understand how the legality plan can be related to the atypicality level of evidence, without exceeding the limits imposed by prohibitions of proof. It is therefore important to see if it is possible to defend the existence of an open criminal procedure in which everything that is not prohibited can be valued as an admissible proof. This is a question applicable to the computer reconstruction of crime, as a new form of scientific criminal evidence with a potential vocation to constitute itself as a legitimate means of proof. The purpose of this dissertation is to explore the contrast between legality and freedom of evidence and its repercussion on the question of the admissibility of the computer reconstruction of crime as a means of proof in the Portuguese Criminal Procedure and, subsequently, to understand what the applicable regime to this new proof instrument, taking into account the need to ensure compliance with legally established procedural safeguards.
A presente dissertação versa sobre a matéria das provas atípicas em Processo Penal, em geral, e sobre a admissibilidade da prova por reconstituição do facto feita por meios informáticos, em particular. O enquadramento geral das provas atípicas no sistema processual penal português é fundamental para perceber de que forma o plano da legalidade se pode relacionar com o plano da atipicidade da prova, sem ultrapassar os limites impostos pelas proibições de prova. É, portanto, importante perceber se é possível defender a existência de um processo penal aberto no qual tudo o que não for proibido possa ser valorado como meio de prova admissível. Trata-se de uma questão aplicável à reconstituição informática do crime, como nova modalidade da prova penal científica com uma vocação potencial para se constituir como meio de prova legítimo. O objectivo desta dissertação será, portanto, o de explorar a contraposição existente entre a legalidade e a liberdade de prova e a sua repercussão na questão da admissibilidade da reconstituição informática do crime como meio de prova no Processo Penal português e, subsequentemente, perceber qual o regime aplicável a este novo instrumento probatório, considerando a necessidade de assegurar o respeito pelas garantias processuais legalmente previstas.

Style APA, Harvard, Vancouver, ISO itp.

Książki na temat "Proof reconstruction"

Trinity and process: A critical evaluation and reconstruction of Hartshorne's di-polar theism towards a trinitarian metaphysics. New York: P. Lang, 1992.

Znajdź pełny tekst źródła

Style APA, Harvard, Vancouver, ISO itp.

Caccamo, Francesco, Pavel Helan i Massimo Tria, red. Primavera di Praga, risveglio europeo. Florence: Firenze University Press, 2011. http://dx.doi.org/10.36253/978-88-6453-271-4.

Pełny tekst źródła

Streszczenie:

The passage of time has not dulled the interest and fascination of the Prague Spring. Proof of this was provided on the occasion of the celebrations for the fortieth anniversary of the events in Czechoslovakia in 1968, greeted all over Europe including Italy by a packed programme of conferences, exhibitions and publications. This book too stemmed from an initiative organised to mark the anniversary, the conference entitled Primavera di Praga, risveglio europeo. Through the reflections of twelve Italian and Czech writers, it aims to help in the recollection and reconstruction of what was, despite its limitations and contradictions, at once the most considered and the most generous attempt at reform of real socialism.

Style APA, Harvard, Vancouver, ISO itp.

Disaster-Proof! Rourke Educational Media, 2017.

Znajdź pełny tekst źródła

Style APA, Harvard, Vancouver, ISO itp.

Koontz, Robin. Disaster-Proof! Rourke Educational Media, 2017.

Znajdź pełny tekst źródła

Style APA, Harvard, Vancouver, ISO itp.

Disaster-Proof! Rourke Educational Media, 2017.

Znajdź pełny tekst źródła

Style APA, Harvard, Vancouver, ISO itp.

Schmitt, Stephanie. Proof Reconstruction in Classical and Non-Classical Logics. Ios Pr Inc, 2000.

Znajdź pełny tekst źródła

Style APA, Harvard, Vancouver, ISO itp.

Reconstructing history: Essays in honour of Prof. V.C. Srivastava. Varanasi: Felicitation Committee, 1998.

Znajdź pełny tekst źródła

Style APA, Harvard, Vancouver, ISO itp.

Misra, Vidya Dhar. Reconstructing History (Essays in Honour of Prof. V.C. Srivastava) - 2 vol. South Asia Books, 1996.

Znajdź pełny tekst źródła

Style APA, Harvard, Vancouver, ISO itp.

Lohwasser, Nelo, i Rainer Schreg, red. Kleine Funde, große Geschichten - Archäologische Funde aus dem Bamberger Dom. University of Bamberg Press, 2021. http://dx.doi.org/10.20378/irb-50035.

Pełny tekst źródła

Streszczenie:

Der Bamberger Dom, das bedeutendste Bauwerk der Stadt, besteht seit gut 1000 Jahren. Prof. Dr. Walter Sage, nachmalig erster Inhaber des Lehrstuhls für Archäologie des Mittelalters und der Neuzeit (AMANZ) an der Universität Bamberg, führte dort von 1969-72 großangelegte Ausgrabungen durch. Er ließ nahezu das gesamte Hauptschiff öffnen, dazu große Bereiche der Seitenschiffe. Man traf Fundamente aller Bauphasen an, dazu viele Bestattungen und eine große Zahl von Kleinfunden. Diese Funde stammen zum Teil von der Innenausstattung des ersten Doms, dessen grundsätzliche Boden- und Wandgestaltung somit gut rekonstruierbar ist. Die wissenschaftliche Aufarbeitung der Funde – 50 Jahre nach ihrer Bergung – war Anlass und Inhalt einer Sonderausstellung im Historischen Museum, bewerkstelligt vom Lehrstuhl AMANZ in Zusammenarbeit mit dem Historischen Verein und dem Historischen Museum Bamberg, den Eigentümern der Funde und unterstützt vom Erzbistum Bamberg. Mit dieser Ausstellung und dem Begleitheft, beides hauptsächlich von Studierenden erarbeitet, feiert der Lehrstuhl AMANZ zudem sein 40-jähriges Bestehen. Bamberg Cathedral, the most important building in the city, was built more than 1000 years ago. Prof. Dr. Walter Sage, who later became the first professor of medieval and postmedieval archaeology at the University of Bamberg, carried out large-scale excavations from 1969-72. He researched almost the entire nave as well as large areas of the aisles. Foundations of all construction phases were found, as well as many burials and a large number of small finds. Many finds were part of the interior of the first cathedral, allowing a reconstruction of the floor and the wall design. 50 years after the excavations the analysis of these finds is part of a new scientific project. Together with the 40th anniversary of the chair of medieval and postmedieval archaeology this is the occasion for a special exhibition in the Historical Museum Bamberg. The exhibition and this booklet were realized in cooperation with the Bamberg Historical Association, who owns the finds today, and with the support of the Archdiocese of Bamberg. Conception, exhibition texts as well as most of the article were prepared by students of the chair of medieval and postmedieval archaeology.

Style APA, Harvard, Vancouver, ISO itp.

Części książek na temat "Proof reconstruction"

Schurr, Hans-Jörg, Mathias Fleury i Martin Desharnais. "Reliable Reconstruction of Fine-grained Proofs in a Proof Assistant". W Automated Deduction – CADE 28, 450–67. Cham: Springer International Publishing, 2021. http://dx.doi.org/10.1007/978-3-030-79876-5_26.

Pełny tekst źródła

Streszczenie:

AbstractWe present a fast and reliable reconstruction of proofs generated by the SMT solver veriT in Isabelle. The fine-grained proof format makes the reconstruction simple and efficient. For typical proof steps, such as arithmetic reasoning and skolemization, our reconstruction can avoid expensive search. By skipping proof steps that are irrelevant for Isabelle, the performance of proof checking is improved. Our method increases the success rate of Sledgehammer by halving the failure rate and reduces the checking time by 13%. We provide a detailed evaluation of the reconstruction time for each rule. The runtime is influenced by both simple rules that appear very often and common complex rules.

Style APA, Harvard, Vancouver, ISO itp.

Reeves, Joseph E., Benjamin Kiesl-Reiter i Marijn J. H. Heule. "Propositional Proof Skeletons". W Tools and Algorithms for the Construction and Analysis of Systems, 329–47. Cham: Springer Nature Switzerland, 2023. http://dx.doi.org/10.1007/978-3-031-30823-9_17.

Pełny tekst źródła

Streszczenie:

AbstractModern SAT solvers produce proofs of unsatisfiability to justify the correctness of their results. These proofs, which are usually represented in the well-known DRAT format, can often become huge, requiring multiple gigabytes of disk storage. We present a technique for semantic proof compression that selects a subset of important clauses from a proof and stores them as a so-called proof skeleton. This proof skeleton can later be used to efficiently reconstruct a full proof by exploiting parallelism. We implemented our approach on top of the award-winning SAT solver CaDiCaL and the proof checker DRAT-trim. In an experimental evaluation, we demonstrate that we can compress proofs into skeletons that are 100 to 5, 000 times smaller than the original proofs. For almost all problems, proof reconstruction using a skeleton improves the solving time on a single core, and is around five times faster when using 24 cores.

Style APA, Harvard, Vancouver, ISO itp.

Schmitt, Stephan, i Christoph Kreitz. "Deleting Redundancy in Proof Reconstruction". W Lecture Notes in Computer Science, 262–76. Berlin, Heidelberg: Springer Berlin Heidelberg, 1998. http://dx.doi.org/10.1007/3-540-69778-0_27.

Pełny tekst źródła

Style APA, Harvard, Vancouver, ISO itp.

Kaliszyk, Cezary, i Josef Urban. "PRocH: Proof Reconstruction for HOL Light". W Automated Deduction – CADE-24, 267–74. Berlin, Heidelberg: Springer Berlin Heidelberg, 2013. http://dx.doi.org/10.1007/978-3-642-38574-2_18.

Pełny tekst źródła

Style APA, Harvard, Vancouver, ISO itp.

Andreotti, Bruno, Hanna Lachnitt i Haniel Barbosa. "Carcara: An Efficient Proof Checker and Elaborator for SMT Proofs in the Alethe Format". W Tools and Algorithms for the Construction and Analysis of Systems, 367–86. Cham: Springer Nature Switzerland, 2023. http://dx.doi.org/10.1007/978-3-031-30823-9_19.

Pełny tekst źródła

Streszczenie:

AbstractProofs from SMT solvers ensure correctness independently from implementation, which is often a requirement when solvers are used in safety-critical applications or proof assistants. Alethe is an established SMT proof format generated by the solvers veriT and cvc5, with reconstruction support in the proof assistants Isabelle/HOL and Coq. The format is close to SMT-LIB and allows both coarse- and fine-grained steps, facilitating proof production. However, it lacks a stand-alone checker, which harms its usability and hinders its adoption. Moreover, the coarse-grained steps can be too expensive to check and lead to verification failures. We present Carcara, an independent proof checker and elaborator for Alethe, implemented in Rust. It aims to increase the adoption of the format by providing push-button proof-checking for Alethe proofs, focusing on efficiency and usability; and by providing elaboration for coarse-grained steps into fine-grained ones, increasing the potential success rate of checking Alethe proofs in performance-critical validators, such as proof assistants. We evaluate Carcara over a large set of Alethe proofs generated from SMT-LIB problems and show that it has good performance and its elaboration techniques can make proofs easier to check.

Style APA, Harvard, Vancouver, ISO itp.

Böhme, Sascha, i Tjark Weber. "Fast LCF-Style Proof Reconstruction for Z3". W Interactive Theorem Proving, 179–94. Berlin, Heidelberg: Springer Berlin Heidelberg, 2010. http://dx.doi.org/10.1007/978-3-642-14052-5_14.

Pełny tekst źródła

Style APA, Harvard, Vancouver, ISO itp.

Montoro, Bárbara, i Pedro Ferradas. "Research and application of earthquake-proof technology". W Disaster Risk Management and Reconstruction in Latin America, 29–36. Rugby, Warwickshire, United Kingdom: Practical Action Publishing, 2014. http://dx.doi.org/10.3362/9781780446721.002.

Pełny tekst źródła

Style APA, Harvard, Vancouver, ISO itp.

Altenkirch, Thorsten, Martin Hofmann i Thomas Streicher. "Categorical reconstruction of a reduction free normalization proof". W Category Theory and Computer Science, 182–99. Berlin, Heidelberg: Springer Berlin Heidelberg, 1995. http://dx.doi.org/10.1007/3-540-60164-3_27.

Pełny tekst źródła

Style APA, Harvard, Vancouver, ISO itp.

Wernhard, Christoph, i Wolfgang Bibel. "Learning from Łukasiewicz and Meredith: Investigations into Proof Structures". W Automated Deduction – CADE 28, 58–75. Cham: Springer International Publishing, 2021. http://dx.doi.org/10.1007/978-3-030-79876-5_4.

Pełny tekst źródła

Streszczenie:

AbstractThe material presented in this paper contributes to establishing a basis deemed essential for substantial progress in Automated Deduction. It identifies and studies global features in selected problems and their proofs which offer the potential of guiding proof search in a more direct way. The studied problems are of the wide-spread form of “axiom(s) and rule(s) imply goal(s)”. The features include the well-known concept of lemmas. For their elaboration both human and automated proofs of selected theorems are taken into a close comparative consideration. The study at the same time accounts for a coherent and comprehensive formal reconstruction of historical work by Łukasiewicz, Meredith and others. First experiments resulting from the study indicate novel ways of lemma generation to supplement automated first-order provers of various families, strengthening in particular their ability to find short proofs.

Style APA, Harvard, Vancouver, ISO itp.

Lachnitt, Hanna, Mathias Fleury, Leni Aniva, Andrew Reynolds, Haniel Barbosa, Andres Nötzli, Clark Barrett i Cesare Tinelli. "IsaRare: Automatic Verification of SMT Rewrites in Isabelle/HOL". W Tools and Algorithms for the Construction and Analysis of Systems, 311–30. Cham: Springer Nature Switzerland, 2024. http://dx.doi.org/10.1007/978-3-031-57246-3_17.

Pełny tekst źródła

Streszczenie:

AbstractSatisfiability modulo theories (SMT) solvers are widely used to ensure the correctness of safety- and security-critical applications. Therefore, being able to trust a solver’s results is crucial. One way to increase trust is to generate independently checkable proof certificates, which record the reasoning steps done by the solver. A key challenge with this approach is that it is difficult to efficiently and accurately produce proofs for reasoning steps involving term rewriting rules. Previous work showed how a domain-specific language, Rare, can be used to capture rewriting rules for the purposes of proof production. However, in that work, the Rare rules had to be trusted, as the correctness of the rules themselves was not checked by the proof checker. In this paper, we present IsaRare, a tool that can automatically translate Rare rules into Isabelle/HOL lemmas. The soundness of the rules can then be verified by proving the lemmas. Because an incorrect rule can put the entire soundness of a proof system in jeopardy, our solution closes an important gap in the trustworthiness of SMT proof certificates. The same tool also provides a necessary component for enabling full proof reconstruction of SMT proof certificates in Isabelle/HOL. We evaluate our approach by verifying an extensive set of rewrite rules used by the cvc5 SMT solver.

Style APA, Harvard, Vancouver, ISO itp.

Streszczenia konferencji na temat "Proof reconstruction"

Blanco, Roberto, Dale Miller i Alberto Momigliano. "Property-Based Testing via Proof Reconstruction". W PPDP '19: Principles and Practice of Programming Languages 2019. New York, NY, USA: ACM, 2019. http://dx.doi.org/10.1145/3354166.3354170.

Pełny tekst źródła

Style APA, Harvard, Vancouver, ISO itp.

"A mathematical proof of a noise weighted FBP reconstruction algorithm". W 2013 IEEE Nuclear Science Symposium and Medical Imaging Conference (2013 NSS/MIC). IEEE, 2013. http://dx.doi.org/10.1109/nssmic.2013.6829219.

Pełny tekst źródła

Style APA, Harvard, Vancouver, ISO itp.

Paez, Gonzalo, i Marija Strojnik. "Phase reconstruction from undersampled intensity pattern(s): uniqueness and convergence proof". W International Conference on Optical Metrology, redaktorzy Malgorzata Kujawinska i Mitsuo Takeda. SPIE, 1999. http://dx.doi.org/10.1117/12.357728.

Pełny tekst źródła

Style APA, Harvard, Vancouver, ISO itp.

Tatum, Marcus, Geb W. Thomas i Donald D. Anderson. "DESIGN AND EVALUATION OF A SYSTEM FOR CT-FREE VOLUME RECONSTRUCTION FROM INTRA-OPERATIVE FLUOROSCOPY FOR NAVIGATION IN ORTHOPEDIC SURGERY". W 2023 Design of Medical Devices Conference. American Society of Mechanical Engineers, 2023. http://dx.doi.org/10.1115/dmd2023-9640.

Pełny tekst źródła

Streszczenie:

Abstract A novel biomechanical guidance system (BGS) for markerless intra-operative bone tracking that seamlessly integrates into the surgical setting was recently developed [1]. It utilizes 3D models from pre-operative CT, via 3D-to-2D registration methods, to update object poses based on 2D fluoroscopic images. However, on occasion pre-operative CT images may be unavailable. We developed a CT-free method to enable BGS use that leverages neural radiance fields (NeRF) to generate a continuous volumetric scene [2,3] from intra-operative fluoroscopy. For proof of concept, digitally reconstructed radiographs (DRRs) were created from pelvic CT data as a stand-in for intra-operative fluoroscopy. DRRs and virtual C-arm positions were fed into an existing NeRF scene reconstruction system,[2,3] and bones were segmented from the reconstruction. The accuracy of NeRF-derived segmentations was evaluated by comparison to gold-standard CT segmentation. The number of input DRRs was varied to study how this parameter influences reconstructions. Volume reconstructions were readily obtained using the NeRF scene reconstruction system. RMS errors of the NeRF-derived segmentations ranged from 1.23 mm when using 36 input DRR images to 1.98 mm when using only 8 input DRR images. Based on this performance, we conclude that CT-free NeRF volume reconstruction from intra-operative fluoroscopy holds great potential for use in surgical navigation applications involving bony procedures.

Style APA, Harvard, Vancouver, ISO itp.

Kosasih, R. "3D reconstruction of abdominal aortic aneurysm using Laplacian Eigenmaps". W THE 2ND NATIONAL CONFERENCE ON MATHEMATICS EDUCATION (NACOME) 2021: Mathematical Proof as a Tool for Learning Mathematics. AIP Publishing, 2023. http://dx.doi.org/10.1063/5.0114420.

Pełny tekst źródła

Style APA, Harvard, Vancouver, ISO itp.

Nguyen, Hung T., Vladik Kreinovich i Olga Kosheleva. "Membership functions representing a number vs. representing a set: Proof of unique reconstruction". W 2016 IEEE International Conference on Fuzzy Systems (FUZZ-IEEE). IEEE, 2016. http://dx.doi.org/10.1109/fuzz-ieee.2016.7737749.

Pełny tekst źródła

Style APA, Harvard, Vancouver, ISO itp.

Brown, Matthew, Valerian Thiel, Markus Allgaier, Michael Raymer, Brian Smith, Paul Kwiat i John Monnier. "Proof-of-Principle Laboratory Demonstration of Long-Baseline Interferometric Imaging Using Distributed Single-Photons". W Quantum 2.0. Washington, D.C.: Optica Publishing Group, 2022. http://dx.doi.org/10.1364/quantum.2022.qm3c.1.

Pełny tekst źródła

Streszczenie:

We report results of very-long-baseline interferometric imaging using distributed single photons. We demonstrate source autocorrelation reconstruction, and increased signal-to-noise ratio per detected coincidence compared to using classical states as phase reference.

Style APA, Harvard, Vancouver, ISO itp.

Shi, Daxin. "Derivation of FBP Reconstruction Algorithm along π-lines Using Katsevich-Type of Proof in Helical CT". W 2019 IEEE Nuclear Science Symposium and Medical Imaging Conference (NSS/MIC). IEEE, 2019. http://dx.doi.org/10.1109/nss/mic42101.2019.9059778.

Pełny tekst źródła

Style APA, Harvard, Vancouver, ISO itp.

Holter, Christian. "Three Years Experience With Solar Air Condition in the EAR Office Tower in Pristina/Kosovo". W ASME 2005 International Solar Energy Conference. ASMEDC, 2005. http://dx.doi.org/10.1115/isec2005-76255.

Pełny tekst źródła

Streszczenie:

Since 2002 the Nine-story building of the headquarters of the European Agency for the Reconstruction of Kosovo is equipped with a solar thermal driven heating and cooling system. The performance fulfils the expectations fully and proof the chosen design and sizing of the system. Solar energy can cover around 75% of the cooling demand and a reasonable fraction of the heating too.

Style APA, Harvard, Vancouver, ISO itp.

Saey, Philippe, Frederic Depuydt, Mathieu Troch, Annemarie Kokosy, Stijn Noppe i Jos Knockaert. "Networked sensing architecture using oversampling techniques in PROFINET IRT devices and isochronous mode processing: Proof-of-principle and signal reconstruction at IO Controller side". W 2017 22nd IEEE International Conference on Emerging Technologies and Factory Automation (ETFA). IEEE, 2017. http://dx.doi.org/10.1109/etfa.2017.8247766.

Pełny tekst źródła

Style APA, Harvard, Vancouver, ISO itp.

Raporty organizacyjne na temat "Proof reconstruction"

Gershoni, Jonathan M., David E. Swayne, Tal Pupko, Shimon Perk, Alexander Panshin, Avishai Lublin i Natalia Golander. Discovery and reconstitution of cross-reactive vaccine targets for H5 and H9 avian influenza. United States Department of Agriculture, styczeń 2015. http://dx.doi.org/10.32747/2015.7699854.bard.

Pełny tekst źródła

Streszczenie:

Research objectives: Identification of highly conserved B-cell epitopes common to either H5 or H9 subtypes of AI Reconstruction of conserved epitopes from (1) as recombinantimmunogens, and testing their suitability to be used as universal vaccine components by measuring their binding to Influenza vaccinated sera of birds Vaccination of chickens with reconstituted epitopes and evaluation of successful vaccination, clinical protection and viral replication Development of a platform to investigate the dynamics of immune response towards infection or an epitope based vaccine Estimate our ability to focus the immune response towards an epitope-based vaccine using the tool we have developed in (D) Summary: This study is a multi-disciplinary study of four-way collaboration; The SERPL, USDA, Kimron-Israel, and two groups at TAU with the purpose of evaluating the production and implementation of epitope based vaccines against avian influenza (AI). Systematic analysis of the influenza viral spike led to the production of a highly conserved epitope situated at the hinge of the HA antigen designated “cluster 300” (c300). This epitope consists of a total of 31 residues and was initially expressed as a fusion protein of the Protein 8 major protein of the bacteriophagefd. Two versions of the c300 were produced to correspond to the H5 and H9 antigens respectively as well as scrambled versions that were identical with regard to amino acid composition yet with varied linear sequence (these served as negative controls). The recombinantimmunogens were produced first as phage fusions and then subsequently as fusions with maltose binding protein (MBP) or glutathioneS-transferase (GST). The latter were used to immunize and boost chickens at SERPL and Kimron. Furthermore, vaccinated and control chickens were challenged with concordant influenza strains at Kimron and SEPRL. Polyclonal sera were obtained for further analyses at TAU and computational bioinformatics analyses in collaboration with Prof. Pupko. Moreover, the degree of protection afforded by the vaccination was determined. Unfortunately, no protection could be demonstrated. In parallel to the main theme of the study, the TAU team (Gershoni and Pupko) designed and developed a novel methodology for the systematic analysis of the antibody composition of polyclonal sera (Deep Panning) which is essential for the analyses of the humoral response towards vaccination and challenge. Deep Panning is currently being used to monitor the polyclonal sera derived from the vaccination studies conducted at the SEPRL and Kimron.

Style APA, Harvard, Vancouver, ISO itp.

Oferujemy zniżki na wszystkie plany premium dla autorów, których prace zostały uwzględnione w tematycznych zestawieniach literatury. Skontaktuj się z nami, aby uzyskać unikalny kod promocyjny!