Results for 'provers'

15 found
Order:
  1. Computer verification for historians of philosophy.Landon D. C. Elkind - 2022 - Synthese 200 (3):1-28.
    Interactive theorem provers might seem particularly impractical in the history of philosophy. Journal articles in this discipline are generally not formalized. Interactive theorem provers involve a learning curve for which the payoffs might seem minimal. In this article I argue that interactive theorem provers have already demonstrated their potential as a useful tool for historians of philosophy; I do this by highlighting examples of work where this has already been done. Further, I argue that interactive theorem (...) can continue to be useful tools for historians of philosophy in the future; this claim is defended through a more conceptual analysis of what historians of philosophy do that identifies argument reconstruction as a core activity of such practitioners. It is then shown that interactive theorem provers can assist in this core practice by a description of what interactive theorem provers are and can do. If this is right, then computer verification for historians of philosophy is in the offing. (shrink)
    Download  
     
    Export citation  
     
    Bookmark  
  2. Verified completeness in Henkin-style for intuitionistic propositional logic.Huayu Guo, Dongheng Chen & Bruno Bentzen - 2023 - In Bruno Bentzen, Beishui Liao, Davide Liga, Reka Markovich, Bin Wei, Minghui Xiong & Tianwen Xu (eds.), Logics for AI and Law: Joint Proceedings of the Third International Workshop on Logics for New-Generation Artificial Intelligence and the International Workshop on Logic, AI and Law, September 8-9 and 11-12, 2023, Hangzhou. College Publications. pp. 36-48.
    This paper presents a formalization of the classical proof of completeness in Henkin-style developed by Troelstra and van Dalen for intuitionistic logic with respect to Kripke models. The completeness proof incorporates their insights in a fresh and elegant manner that is better suited for mechanization. We discuss details of our implementation in the Lean theorem prover with emphasis on the prime extension lemma and construction of the canonical model. Our implementation is restricted to a system of intuitionistic propositional logic with (...)
    Download  
     
    Export citation  
     
    Bookmark  
  3. The ILLTP Library for Intuitionistic Linear Logic.Carlos Olarte, Valeria Correa Vaz De Paiva, Elaine Pimentel & Giselle Reis - manuscript
    Benchmarking automated theorem proving (ATP) systems using standardized problem sets is a well-established method for measuring their performance. However, the availability of such libraries for non-classical logics is very limited. In this work we propose a library for benchmarking Girard's (propositional) intuitionistic linear logic. For a quick bootstrapping of the collection of problems, and for discussing the selection of relevant problems and understanding their meaning as linear logic theorems, we use translations of the collection of Kleene's intuitionistic theorems in the (...)
    Download  
     
    Export citation  
     
    Bookmark  
  4. Automated Theorem Proving and Its Prospects. [REVIEW]Desmond Fearnley-Sander - 1995 - PSYCHE: An Interdisciplinary Journal of Research On Consciousness 2.
    REVIEW OF: Automated Development of Fundamental Mathematical Theories by Art Quaife. (1992: Kluwer Academic Publishers) 271pp. Using the theorem prover OTTER Art Quaife has proved four hundred theorems of von Neumann-Bernays-Gödel set theory; twelve hundred theorems and definitions of elementary number theory; dozens of Euclidean geometry theorems; and Gödel's incompleteness theorems. It is an impressive achievement. To gauge its significance and to see what prospects it offers this review looks closely at the book and the proofs it presents.
    Download  
     
    Export citation  
     
    Bookmark  
  5. Mereology.Ben Blumson - 2021 - Archive of Formal Proofs.
    The interactive theorem prover Isabelle/HOL is used to verify elementary theorems of classical extensional mereology.
    Download  
     
    Export citation  
     
    Bookmark   2 citations  
  6.  77
    Theorem proving in artificial neural networks: new frontiers in mathematical AI.Markus Pantsar - 2024 - European Journal for Philosophy of Science 14 (1):1-22.
    Computer assisted theorem proving is an increasingly important part of mathematical methodology, as well as a long-standing topic in artificial intelligence (AI) research. However, the current generation of theorem proving software have limited functioning in terms of providing new proofs. Importantly, they are not able to discriminate interesting theorems and proofs from trivial ones. In order for computers to develop further in theorem proving, there would need to be a radical change in how the software functions. Recently, machine learning results (...)
    Download  
     
    Export citation  
     
    Bookmark  
  7. Proof phenomenon as a function of the phenomenology of proving.Inês Hipólito - 2015 - Progress in Biophysics and Molecular Biology 119:360-367.
    Kurt Gödel wrote (1964, p. 272), after he had read Husserl, that the notion of objectivity raises a question: “the question of the objective existence of the objects of mathematical intuition (which, incidentally, is an exact replica of the question of the objective existence of the outer world)”. This “exact replica” brings to mind the close analogy Husserl saw between our intuition of essences in Wesensschau and of physical objects in perception. What is it like to experience a mathematical proving (...)
    Download  
     
    Export citation  
     
    Bookmark   2 citations  
  8. Automating Leibniz’s Theory of Concepts.Paul Edward Oppenheimer, Jesse Alama & Edward N. Zalta - 2015 - In Felty Amy P. & Middeldorp Aart (eds.), Automated Deduction – CADE 25: Proceedings of the 25th International Conference on Automated Deduction (Lecture Notes in Artificial Intelligence: Volume 9195), Berlin: Springer. Springer. pp. 73-97.
    Our computational metaphysics group describes its use of automated reasoning tools to study Leibniz’s theory of concepts. We start with a reconstruction of Leibniz’s theory within the theory of abstract objects (henceforth ‘object theory’). Leibniz’s theory of concepts, under this reconstruction, has a non-modal algebra of concepts, a concept-containment theory of truth, and a modal metaphysics of complete individual concepts. We show how the object-theoretic reconstruction of these components of Leibniz’s theory can be represented for investigation by means of automated (...)
    Download  
     
    Export citation  
     
    Bookmark   5 citations  
  9. A New Three Dimensional Bivalent Hypercube Description, Analysis, and Prospects for Research.Jeremy Horne - 2012 - Neuroquantology 10 (1):12.
    A three dimensional hypercube representing all of the 4,096 dyadic computations in a standard bivalent system has been created. It has been constructed from the 16 functions arrayed in a table of functional completeness that can compute a dyadic relationship. Each component of the dyad is an operator as well as a function, such as “implication” being a result, as well as an operation. Every function in the hypercube has been color keyed to enhance the display of emerging patterns. At (...)
    Download  
     
    Export citation  
     
    Bookmark   1 citation  
  10. A Henkin-style completeness proof for the modal logic S5.Bruno Bentzen - 2021 - In Pietro Baroni, Christoph Benzmüller & Yì N. Wáng (eds.), Logic and Argumentation: Fourth International Conference, CLAR 2021, Hangzhou, China, October 20–22. Springer. pp. 459-467.
    This paper presents a recent formalization of a Henkin-style completeness proof for the propositional modal logic S5 using the Lean theorem prover. The proof formalized is close to that of Hughes and Cresswell, but the system, based on a different choice of axioms, is better described as a Mendelson system augmented with axiom schemes for K, T, S4, and B, and the necessitation rule as a rule of inference. The language has the false and implication as the only primitive logical (...)
    Download  
     
    Export citation  
     
    Bookmark   1 citation  
  11. Duas perspectivas buddhistas sobre a temporalidade e o renascimento.Felipe Nogueira de Carvalho - 2020 - Reflexus 14 (1):177-200.
    A doutrina do renascimento transmite a ideia de uma perspectiva temporal mais extensa, que abarca múltiplas vidas. Mas a medida em que o buddhismo chega à modernidade, outras interpretações começam a aparecer. Um exemplo é a interpretação psicológica de Ajahn Buddhadāsa, segundo a qual o termo “renascimento" se refere ao surgimento sucessivo da ideia do “eu" a cada instante de consciência. Esta interpretação diminui consideravelmente a extensão da perspectiva temporal ligada ao renascimento. Contra esta interpretação, Thānissaro Bhikkhu argumentou que uma (...)
    Download  
     
    Export citation  
     
    Bookmark  
  12. Estabelecimento da Gestação nos Animais.Emanuel Isaque Cordeiro da Silva - manuscript
    OBJETIVO A gestação nos mamíferos domésticos é um processo fisiológico que implica mudanças físicas, metabólicas e hormonais na fêmea, que culminam com o nascimento de um novo indivíduo. Desta forma, a compreensão de tais mudanças e como estas favorecem um ambiente ideal de desenvolvimento embrionário inicial, até a placentação e a fisiologia envolvidas durante esses processos é fundamental na tomada de decisões quanto à saúde reprodutiva da fêmea, na seleção de futuras matrizes e até mesmo para a saúde fetal e (...)
    Download  
     
    Export citation  
     
    Bookmark  
  13. Deepening the Automated Search for Gödel's Proofs.Adam Conkey - unknown
    Gödel's incompleteness theorems establish the stunning result that mathematics cannot be fully formalized and, further, that any formal system containing a modicum of number or set theory cannot establish its own consistency. Wilfried Sieg and Clinton Field, in their paper Automated Search for Gödel's Proofs, presented automated proofs of Gödel's theorems at an abstract axiomatic level; they used an appropriate expansion of the strategic considerations that guide the search of the automated theorem prover AProS. The representability conditions that allow the (...)
    Download  
     
    Export citation  
     
    Bookmark  
  14. A Consolidação da Sociedade Capitalista e a Ciência da Sociedade.Emanuel Isaque Cordeiro da Silva - manuscript
    PREMISSA No século XIX, ocorreram transformações impulsionadas pela emergência de novas fontes energéticas (água e petróleo), por novos ramos industriais e pela alteração profunda nos processos produtivos, com a introdução de novas máquinas e equipamentos. Depois de 300 anos de exploração por parte das nações europeias, iniciou -se, principalmente nas colônias latino-americanas, um processo intenso de lutas pela independência. É no século XIX, já com a consolidação do sistema capitalista na Europa, que se encontra a herança intelectual mais próxima da (...)
    Download  
     
    Export citation  
     
    Bookmark  
  15. A Educação de Jovens e Adultos como Transformação Social.Emanuel Isaque Cordeiro da Silva & Meuri Rusy Maria do Nascimento - 2017 - Dissertation,
    Monografia apresentada à banca examinadora da Escola Municipal Manuel Teodoro de Arruda, anexa do Colégio Frei Cassiano de Comacchio em Belo Jardim, para a obtenção do título de concluinte do curso de Normal Médio, oferecido pela instituição. A natureza do trabalho, em suma, consiste em apresentar perspectivas de trans formação social para a comunidade de jovens e adultos, o principal programa cunho do trabalho é a Educação de Jovens e Adultos a EJA, e como esse programa intervém na sociabilidade e (...)
    Download  
     
    Export citation  
     
    Bookmark