Relevant bibliographies by topics / Proof reconstruction

Contents

  1. Journal articles
  2. Dissertations / Theses
  3. Books
  4. Book chapters
  5. Conference papers
  6. Reports

Academic literature on the topic 'Proof reconstruction'

Author: Grafiati
Published: 25 May 2024

Create a spot-on reference in APA, MLA, Chicago, Harvard, and other styles

Select a source type:

Consult the lists of relevant articles, books, theses, conference reports, and other scholarly sources on the topic 'Proof reconstruction.'

Next to every source in the list of references, there is an 'Add to bibliography' button. Press on it, and we will generate automatically the bibliographic reference to the chosen work in the citation style you need: APA, MLA, Harvard, Chicago, Vancouver, etc.

You can also download the full text of the academic publication as pdf and read online its abstract whenever available in the metadata.

Journal articles on the topic "Proof reconstruction"

1

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

Full text
Abstract:
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.
APA, Harvard, Vancouver, ISO, and other styles
2

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

Full text
APA, Harvard, Vancouver, ISO, and other styles
3

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

Full text
APA, Harvard, Vancouver, ISO, and other styles
4

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

Full text
Abstract:
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.
APA, Harvard, Vancouver, ISO, and other styles
5

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

Full text
APA, Harvard, Vancouver, ISO, and other styles
6

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

Full text
Abstract:
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.
APA, Harvard, Vancouver, ISO, and other styles
7

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

Full text
Abstract:
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.
APA, Harvard, Vancouver, ISO, and other styles
8

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

Full text
Abstract:
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.
APA, Harvard, Vancouver, ISO, and other styles
9

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

Full text
Abstract:
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.
APA, Harvard, Vancouver, ISO, and other styles
10

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

Full text
Abstract:
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.
APA, Harvard, Vancouver, ISO, and other styles
More sources

Dissertations / Theses on the topic "Proof reconstruction"

1

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

Full text
Abstract:
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
APA, Harvard, Vancouver, ISO, and other styles
2

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.

Full text
APA, Harvard, Vancouver, ISO, and other styles
3

Last, Carsten [Verfasser], and 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.

Full text
APA, Harvard, Vancouver, ISO, and other styles
4

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.

Full text
Abstract:
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.
APA, Harvard, Vancouver, ISO, and other styles

Books on the topic "Proof reconstruction"

1

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

Find full text
APA, Harvard, Vancouver, ISO, and other styles
2

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

Full text
Abstract:
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.
APA, Harvard, Vancouver, ISO, and other styles
3

Disaster-Proof! Rourke Educational Media, 2017.

Find full text
APA, Harvard, Vancouver, ISO, and other styles
4

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

Find full text
APA, Harvard, Vancouver, ISO, and other styles
5

Disaster-Proof! Rourke Educational Media, 2017.

Find full text
APA, Harvard, Vancouver, ISO, and other styles
6

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

Find full text
APA, Harvard, Vancouver, ISO, and other styles
7

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

Find full text
APA, Harvard, Vancouver, ISO, and other styles
8

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

Find full text
APA, Harvard, Vancouver, ISO, and other styles
9

Lohwasser, Nelo, and Rainer Schreg, eds. 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.

Full text
Abstract:
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.
APA, Harvard, Vancouver, ISO, and other styles

Book chapters on the topic "Proof reconstruction"

1

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

Full text
Abstract:
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.
APA, Harvard, Vancouver, ISO, and other styles
2

Reeves, Joseph E., Benjamin Kiesl-Reiter, and Marijn J. H. Heule. "Propositional Proof Skeletons." In 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.

Full text
Abstract:
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.
APA, Harvard, Vancouver, ISO, and other styles
3

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

Full text
APA, Harvard, Vancouver, ISO, and other styles
4

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

Full text
APA, Harvard, Vancouver, ISO, and other styles
5

Andreotti, Bruno, Hanna Lachnitt, and Haniel Barbosa. "Carcara: An Efficient Proof Checker and Elaborator for SMT Proofs in the Alethe Format." In 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.

Full text
Abstract:
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.
APA, Harvard, Vancouver, ISO, and other styles
6

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

Full text
APA, Harvard, Vancouver, ISO, and other styles
7

Montoro, Bárbara, and Pedro Ferradas. "Research and application of earthquake-proof technology." In 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.

Full text
APA, Harvard, Vancouver, ISO, and other styles
8

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

Full text
APA, Harvard, Vancouver, ISO, and other styles
9

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

Full text
Abstract:
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.
APA, Harvard, Vancouver, ISO, and other styles
10

Lachnitt, Hanna, Mathias Fleury, Leni Aniva, Andrew Reynolds, Haniel Barbosa, Andres Nötzli, Clark Barrett, and Cesare Tinelli. "IsaRare: Automatic Verification of SMT Rewrites in Isabelle/HOL." In 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.

Full text
Abstract:
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.
APA, Harvard, Vancouver, ISO, and other styles

Conference papers on the topic "Proof reconstruction"

1

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

Full text
APA, Harvard, Vancouver, ISO, and other styles
2

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

Full text
APA, Harvard, Vancouver, ISO, and other styles
3

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

Full text
APA, Harvard, Vancouver, ISO, and other styles
4

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

Full text
Abstract:
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.
APA, Harvard, Vancouver, ISO, and other styles
5

Kosasih, R. "3D reconstruction of abdominal aortic aneurysm using Laplacian Eigenmaps." In 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.

Full text
APA, Harvard, Vancouver, ISO, and other styles
6

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

Full text
APA, Harvard, Vancouver, ISO, and other styles
7

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

Full text
Abstract:
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.
APA, Harvard, Vancouver, ISO, and other styles
8

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

Full text
APA, Harvard, Vancouver, ISO, and other styles
9

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

Full text
Abstract:
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.
APA, Harvard, Vancouver, ISO, and other styles
10

Saey, Philippe, Frederic Depuydt, Mathieu Troch, Annemarie Kokosy, Stijn Noppe, and 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." In 2017 22nd IEEE International Conference on Emerging Technologies and Factory Automation (ETFA). IEEE, 2017. http://dx.doi.org/10.1109/etfa.2017.8247766.

Full text
APA, Harvard, Vancouver, ISO, and other styles

Reports on the topic "Proof reconstruction"

1

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

Full text
Abstract:
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.
APA, Harvard, Vancouver, ISO, and other styles
You might also be interested in the extended bibliographies on the topic 'Proof reconstruction' for particular source types:
Journal articles
We offer discounts on all premium plans for authors whose works are included in thematic literature selections. Contact us to get a unique promo code!

To the bibliography