Search results for 'Automatic theorem proving' (try it on Scholar)

1000+ found
Order:
  1.  3
    J. A. Robinson (1974). A Review of Automatic Theorem-Proving. [REVIEW] Journal of Symbolic Logic 39 (1):190-190.
    Direct download  
     
    Export citation  
     
    My bibliography  
  2.  3
    L. Wos (1974). Review: J. A. Robinson, A Review of Automatic Theorem-Proving. [REVIEW] Journal of Symbolic Logic 39 (1):190-190.
    Direct download (2 more)  
     
    Export citation  
     
    My bibliography  
  3.  1
    Frank Pfenning (1989). Review: Jean H. Gallier, Logic for Computer Science. Foundations of Automatic Theorem Proving. [REVIEW] Journal of Symbolic Logic 54 (1):288-289.
    Direct download (2 more)  
     
    Export citation  
     
    My bibliography  
  4.  1
    Tryggvi Edwald (1990). The T‐Variable Method in Gentzen‐Style Automatic Theorem Proving. Mathematical Logic Quarterly 36 (3):253-261.
    Direct download (3 more)  
     
    Export citation  
     
    My bibliography  
  5. Tryggvi Edwald (1990). The T-Variable Method in Gentzen-Style Automatic Theorem Proving. Zeitschrift fur mathematische Logik und Grundlagen der Mathematik 36 (3):253-261.
    No categories
    Direct download (2 more)  
     
    Export citation  
     
    My bibliography  
  6. Joyce Friedman (1974). Review: Hao Wang, Wayne A. Kalenich, Formalization and Automatic Theorem-Proving. [REVIEW] Journal of Symbolic Logic 39 (2):350-350.
  7. Czeslaw Lejewski & Zdzislaw Pawlak (1967). Automatic Theorem-Proving. Philosophical Quarterly 17 (69):369.
  8. Lawrence T. Wos (1970). Review: James R. Slagle, Automatic Theorem Proving with Renamable and Semantic Resolution. [REVIEW] Journal of Symbolic Logic 35 (4):595-596.
    Direct download  
     
    Export citation  
     
    My bibliography  
  9. Chin-Liang Chang (1973/1987). Symbolic Logic and Mechanical Theorem Proving. Academic Press.
    This book contains an introduction to symbolic logic and a thorough discussion of mechanical theorem proving and its applications. The book consists of three major parts. Chapters 2 and 3 constitute an introduction to symbolic logic. Chapters 4–9 introduce several techniques in mechanical theorem proving, and Chapters 10 an 11 show how theorem proving can be applied to various areas such as question answering, problem solving, program analysis, and program synthesis.
     
    Export citation  
     
    My bibliography   13 citations  
  10. Paul B. Thistlewaite, M. A. Mcrobbie & Robert K. Meyer (1988). Automated Theorem-Proving in Non-Classical Logics. Monograph Collection (Matt - Pseudo).
     
    Export citation  
     
    My bibliography   7 citations  
  11. Melvin Fitting (1998). First-Order Logic and Automated Theorem Proving. Studia Logica 61 (2):300-302.
     
    Export citation  
     
    My bibliography   5 citations  
  12. Michael J. C. Gordon & T. F. Melham (1993). Introduction to Hol a Theorem Proving Environment for Higher Order Logic. Monograph Collection (Matt - Pseudo).
     
    Export citation  
     
    My bibliography  
  13. J. Grundy & Malcolm Charles Newey (1998). Theorem Proving in Higher Order Logics 11th International Conference, Tphols '98, Canberra, Australia, September 27-October 2, 1998 : Proceedings'. [REVIEW]
     
    Export citation  
     
    My bibliography  
  14. J. Grundy & Malcolm Charles Newey (1998). Theorem Proving in Higher Order Logics : Emerging Trends 11th International Conference, Tphols '98, Canberra, Australia, September 27-October 2, 1997 ; Supplementary Proceedings'. [REVIEW]
     
    Export citation  
     
    My bibliography  
  15. Dominique Snyers & André Thayse (1987). From Logic Design to Logic Programming Theorem Proving Techniques and P-Functions.
     
    Export citation  
     
    My bibliography  
  16.  3
    Carlo Cellucci (forthcoming). Is Mathematics Problem Solving or Theorem Proving? Foundations of Science:1-17.
    The question that is the subject of this article is not intended to be a sociological or statistical question about the practice of today’s mathematicians, but a philosophical question about the nature of mathematics, and specifically the method of mathematics. Since antiquity, saying that mathematics is problem solving has been an expression of the view that the method of mathematics is the analytic method, while saying that mathematics is theorem proving has been an expression of the view that (...)
    Direct download (2 more)  
     
    Export citation  
     
    My bibliography  
  17. Sueli Mendes dos Santos (1972). Automatic Proofs for Theorems on Predicate Calculus. [Rio De Janeiro,Pontificia Universidade Católica Do Rio De Janeiro].
     
    Export citation  
     
    My bibliography  
  18.  4
    Furio Di Paola (1988). Human-Oriented and Machine-Oriented Reasoning: Remarks on Some Problems in the History of Automated Theorem Proving. [REVIEW] AI and Society 2 (2):121-131.
    Examples in the history of Automated Theorem Proving are given, in order to show that even a seemingly ‘mechanical’ activity, such as deductive inference drawing, involves special cultural features and tacit knowledge. Mechanisation of reasoning is thus regarded as a complex undertaking in ‘cultural pruning’ of human-oriented reasoning. Sociological counterparts of this passage from human- to machine-oriented reasoning are discussed, by focusing on problems of man-machine interaction in the area of computer-assisted proof processing.
    Direct download (3 more)  
     
    Export citation  
     
    My bibliography  
  19. N. Shankar (1994). Metamathematics, Machines, and Gödel's Proof. Cambridge University Press.
    The automatic verification of large parts of mathematics has been an aim of many mathematicians from Leibniz to Hilbert. While Gödel's first incompleteness theorem showed that no computer program could automatically prove certain true theorems in mathematics, the advent of electronic computers and sophisticated software means in practice there are many quite effective systems for automated reasoning that can be used for checking mathematical proofs. This book describes the use of a computer program to check the proofs of (...)
     
    Export citation  
     
    My bibliography   1 citation  
  20.  28
    Alexander Koller, Ralph Debusmann, Malte Gabsdil & Kristina Striegnitz (2004). Put My Galakmid Coin Into the Dispenser and Kick It: Computational Linguistics and Theorem Proving in a Computer Game. [REVIEW] Journal of Logic, Language and Information 13 (2):187-206.
    We combine state-of-the-art techniques from computational linguisticsand theorem proving to build an engine for playing text adventures,computer games with which the player interacts purely through naturallanguage. The system employs a parser for dependency grammar and ageneration system based on TAG, and has components for resolving andgenerating referring expressions. Most of these modules make heavy useof inferences offered by a modern theorem prover for descriptionlogic. Our game engine solves some problems inherent in classical textadventures, and is an interesting (...)
    Direct download (8 more)  
     
    Export citation  
     
    My bibliography  
  21. Robert S. Boyer & J. Strother Moore (1988). A Computational Logic Handbook.
     
    Export citation  
     
    My bibliography   1 citation  
  22. Franz Baader (2003). Automated Deduction--Cade-19 19th International Conference on Automated Deduction, Miami Beach, Fl, Usa, July 28-August 2, 2003 : Proceedings. [REVIEW]
  23. G. Gottlob, Alexander Leitsch, Daniele Mundici & Kurt Gödel Society (1993). Computational Logic and Proof Theory Third Kurt Gödel Colloquium, Kgc'93 : Brno, Czech Republic, August 1993 : Proceedings. [REVIEW]
     
    Export citation  
     
    My bibliography  
  24. G. Gottlob, Alexander Leitsch, Daniele Mundici & Kurt Gödel Society (1997). Computational Logic and Proof Theory 5th Kurt Gödel Colloquium, Kgc '97, Vienna, Austria, August 25-29, 1997 : Proceedings'. [REVIEW]
     
    Export citation  
     
    My bibliography  
  25. Jean-Louis Lassez, G. Plotkin & J. A. Robinson (1991). Computational Logic Essays in Honor of Alan Robinson. Monograph Collection (Matt - Pseudo).
     
    Export citation  
     
    My bibliography  
  26. M. A. Mcrobbie & J. K. Slaney (1996). Automated Deduction Cade-13 : 13th International Conference on Automated Deduction, New Brunswick, Nj, Usa, July 30-August 3, 1996 : Proceedings. [REVIEW]
  27. Moshe Y. Vardi & A. Voronkov (2003). Logic for Programming Artificial Intelligence and Reasoning 10th International Conference, Lpar 2003, Almaty, Kazakhstan, September 22-26, 2003 : Proceedings. [REVIEW]
     
    Export citation  
     
    My bibliography  
  28.  2
    Jeremy Avigad, Leonardo de Moura & Soonho Kong, Theorem Proving in Lean.
    Formal verification involves the use of logical and computational methods to establish claims that are expressed in precise mathematical terms. These can include ordinary mathematical theorems, as well as claims that pieces of hardware or software, network protocols, and mechanical and hybrid systems meet their specifications. In practice, there is not a sharp distinction between verifying a piece of mathematics and verifying the correctness of a system: formal verification requires describing hardware and software systems in mathematical terms, at which point (...)
    No categories
    Direct download (2 more)  
     
    Export citation  
     
    My bibliography  
  29.  72
    Michael Kohlhase, Higher-Order Automated Theorem Proving.
    The history of building automated theorem provers for higher-order logic is almost as old as the field of deduction systems itself. The first successful attempts to mechanize and implement higher-order logic were those of Huet [13] and Jensen and Pietrzykowski [17]. They combine the resolution principle for higher-order logic (first studied in [1]) with higher-order unification. The unification problem in typed λ-calculi is much more complex than that for first-order terms, since it has to take the theory of αβη-equality (...)
    Translate
      Direct download  
     
    Export citation  
     
    My bibliography  
  30.  14
    Joseph S. Fulda & Kevin De Fontes (1989). The A Priori Meaningfulness Measure and Resolution Theorem Proving. Journal of Experimental and Theoretical Artificial Intelligence 1 (3):227-230.
    Demonstrates the validity of the measure presented in "Estimating Semantic Content" on textbook examples using (binary) resolution [a generalization of disjunctive syllogism] theorem proving; the measure is based on logical probability and is the mirror image of logical form; it dates to Popper.
    Direct download  
     
    Export citation  
     
    My bibliography  
  31.  3
    Alberto Momigliano, Theorem Proving Via Uniform Proofs>.
    Uniform proofs systems have recently been proposed [Mi191j as a proof-theoretic foundation and generalization of logic programming. In [Mom92a] an extension with constructive negation is presented preserving the nature of abstract logic programming language. Here we adapt this approach to provide a complete theorem proving technique for minimal, intuitionistic and classical logic, which is totally goal-oriented and does not require any form of ancestry resolution. The key idea is to use the Godel-Gentzen translation to embed those logics in (...)
    Direct download (4 more)  
     
    Export citation  
     
    My bibliography  
  32.  25
    Francis J. Pelletier (1993). Identity in Modal Logic Theorem Proving. Studia Logica 52 (2):291 - 308.
    THINKER is an automated natural deduction first-order theorem proving program. This paper reports on how it was adapted so as to prove theorems in modal logic. The method employed is an indirect semantic method, obtained by considering the semantic conditions involved in being a valid argument in these modal logics. The method is extended from propositional modal logic to predicate modal logic, and issues concerning the domain of quantification and existence in a world's domain are discussed. Finally, we (...)
    Direct download (6 more)  
     
    Export citation  
     
    My bibliography  
  33.  2
    Christoph Kreitz & Brigitte Pientka (2001). Connection-Driven Inductive Theorem Proving. Studia Logica 69 (2):293-326.
    We present a method for integrating rippling-based rewriting into matrix-based theorem proving as a means for automating inductive specification proofs. The selection of connections in an inductive matrix proof is guided by symmetries between induction hypothesis and induction conclusion. Unification is extended by decision procedures and a rippling/reverse-rippling heuristic. Conditional substitutions are generated whenever a uniform substitution is impossible. We illustrate the integrated method by discussing several inductive proofs for the integer square root problem as well as the (...)
    Direct download (8 more)  
     
    Export citation  
     
    My bibliography  
  34. Jeremy Pitt & Jim Cunningham (1996). Theorem Proving and Model Building with the Calculus KE. Logic Journal of the Igpl 4 (1):129-150.
    A Prolog implementation of a new theorem-prover for first-order classical logic is described. The prover is based on the calculus KE and the rules used for analysing quantifiers in free variable semantic tableaux. A formal specification of the rules used in the implementation is described, for which soundness and completeness is straightforwardly verified. The prover has been tested on the first 47 problems of the Pelletier set, and its performance compared with a state of the art semantic tableaux (...)-prover. It has also been applied to model building in a prototype system for logical animation, a technique for symbolic execution which can be used for validation. The interest of these experiments is that they demonstrate the value of certain “characteristics” of the KE calculus, such as the significant space-saving in theorem-proving, the mutual inconsistency of open branches in KE trees, and the relation of the KE rules to “traditional” forms of reasoning. (shrink)
    Direct download  
     
    Export citation  
     
    My bibliography  
  35.  10
    Gordon Beavers (1993). Automated Theorem Proving for Łukasiewicz Logics. Studia Logica 52 (2):183 - 195.
    This paper is concerned with decision proceedures for the 0-valued ukasiewicz logics,. It is shown how linear algebra can be used to construct an automated theorem checker. Two decision proceedures are described which depend on a linear programming package. An algorithm is given for the verification of consequence relations in, and a connection is made between theorem checking in two-valued logic and theorem checking in which implies that determing of a -free formula whether it takes the value (...)
    Direct download (5 more)  
     
    Export citation  
     
    My bibliography  
  36. Uwe Petermann (2014). Theorem Proving with Built-in Hybrid Theories. Logic and Logical Philosophy 6:77.
    A growing number of applications of automated reasoning exhibitsthe necessity of flexible deduction systems. A deduction system should beable to execute inference rules which are appropriate to the given problem.One way to achieve this behavior is the integration of different calculi. Thisled to so called hybrid reasoning [22, 1, 10, 20] which means the integrationof a general purpose foreground reasoner with a specialized background reasoner. A typical task of a background reasoner is to perform special purposeinference rules according to a (...)
    Direct download (4 more)  
     
    Export citation  
     
    My bibliography  
  37. Proving in Finite Many-Valued Propositional (forthcoming). An Algorithm for Axiomatizing and Theorem Proving in Finite Many-Valued Propositional Logics* Walter A. Carnielli. Logique Et Analyse.
     
    Export citation  
     
    My bibliography  
  38.  3
    L. Wos, S. Winker, R. Veroff, B. Smith & L. Henschen (1983). Questions Concerning Possible Shortest Single Axioms for the Equivalential Calculus: An Application of Automated Theorem Proving to Infinite Domains. Notre Dame Journal of Formal Logic 24 (2):205-223.
    Direct download (4 more)  
     
    Export citation  
     
    My bibliography   17 citations  
  39.  13
    Jan van Eijck, HyLoTab — Tableau-Based Theorem Proving for Hybrid Logics.
    This paper contains the full code of a prototype implementation in Haskell [5], in ‘literate programming’ style [6], of the tableau-based calculus and proof procedure for hybrid logic presented in [4].
    Translate
      Direct download  
     
    Export citation  
     
    My bibliography   1 citation  
  40.  2
    Jean Flower, Judith Masthoff & Gem Stapleton (2004). Generating Readable Proofs: A Heuristic Approach to Theorem Proving with Spider Diagrams. In A. Blackwell, K. Marriott & A. Shimojima (eds.), Diagrammatic Representation and Inference. Springer 166--181.
    Direct download  
     
    Export citation  
     
    My bibliography   1 citation  
  41. Martin Davis, George Logemann & Donald Loveland (1967). A Machine Program for Theorem-Proving. Journal of Symbolic Logic 32 (1):118-118.
    Direct download  
     
    Export citation  
     
    My bibliography   6 citations  
  42. Eric Livingston (2005). Natural Reasoning in Mathematical Theorem Proving. Communication and Cognition. Monographies 38 (3-4):319-344.
     
    Export citation  
     
    My bibliography  
  43.  4
    Tomás E. Uribe (2000). Combinations of Model Checking and Theorem Proving. In Dov M. Gabbay & Maarten de Rijke (eds.), Frontiers of Combining Systems. Research Studies Press 151--170.
    Direct download (2 more)  
     
    Export citation  
     
    My bibliography  
  44.  7
    Christoph Benzmüller (2002). Comparing Approaches to Resolution Based Higher-Order Theorem Proving. Synthese 133 (1-2):203 - 235.
    We investigate several approaches to resolution based automated theoremproving in classical higher-order logic (based on Church's simply typed-calculus) and discuss their requirements with respect to Henkincompleteness and full extensionality. In particular we focus on Andrews'higher-order resolution (Andrews 1971), Huet's constrained resolution (Huet1972), higher-order E-resolution, and extensional higher-order resolution(Benzmüller and Kohlhase 1997). With the help of examples we illustratethe parallels and differences of the extensionality treatment of these approachesand demonstrate that extensional higher-order resolution is the sole approach thatcan completely avoid additional (...)
    Direct download (7 more)  
     
    Export citation  
     
    My bibliography   1 citation  
  45.  1
    Sebastian Eberhard & Stefan Hetzl (2015). Inductive Theorem Proving Based on Tree Grammars. Annals of Pure and Applied Logic 166 (6):665-700.
    Direct download (2 more)  
     
    Export citation  
     
    My bibliography  
  46.  4
    Mi Lu & Jinzhao Wu (2000). On Theorem Proving in Annotated Logics. Journal of Applied Non-Classical Logics 10 (2):121-143.
    Direct download (4 more)  
     
    Export citation  
     
    My bibliography  
  47.  5
    Nicola Olivetti & Gian Luca Pozzato (2008). Theorem Proving for Conditional Logics: CondLean and GOALD U CK. Journal of Applied Non-Classical Logics 18 (4):427-473.
    Direct download (4 more)  
     
    Export citation  
     
    My bibliography  
  48.  5
    Anita Wasilewska (1985). Some Remarks on Theorem Proving Systems and Mazurkiewicz Algorithms Associated with Them. Mathematical Logic Quarterly 31 (19‐20):289-294.
    Direct download (6 more)  
     
    Export citation  
     
    My bibliography  
  49.  2
    Jeremy George Peterson (1978). An Automatic Theorem Prover for Substitution and Detachment Systems. Notre Dame Journal of Formal Logic 19 (1):119-122.
    Direct download (3 more)  
     
    Export citation  
     
    My bibliography   1 citation  
  50.  1
    J. A. Robinson (1980). Review: Donald W. Loveland, Automated Theorem Proving. A Logical Basis. [REVIEW] Journal of Symbolic Logic 45 (3):629-630.
    Direct download (2 more)  
     
    Export citation  
     
    My bibliography  
1 — 50 / 1000