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

1000+ found
Sort by:
  1. Chin-Liang Chang (1973/1987). Symbolic Logic and Mechanical Theorem Proving. Academic Press.score: 116.0
    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.
     
    My bibliography  
     
    Export citation  
  2. Tryggvi Edwald (1990). The T‐Variable Method in Gentzen‐Style Automatic Theorem Proving. Mathematical Logic Quarterly 36 (3):253-261.score: 90.0
    No categories
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  3. Joyce Friedman (1974). Review: Hao Wang, Wayne A. Kalenich, Formalization and Automatic Theorem-Proving. [REVIEW] Journal of Symbolic Logic 39 (2):350-350.score: 90.0
    Direct download (2 more)  
     
    My bibliography  
     
    Export citation  
  4. Czeslaw Lejewski & Zdzislaw Pawlak (1967). Automatic Theorem-Proving. Philosophical Quarterly 17 (69):369.score: 90.0
    No categories
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  5. 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.score: 90.0
    Direct download (2 more)  
     
    My bibliography  
     
    Export citation  
  6. L. Wos (1974). Review: J. A. Robinson, A Review of Automatic Theorem-Proving. [REVIEW] Journal of Symbolic Logic 39 (1):190-190.score: 90.0
    Direct download (2 more)  
     
    My bibliography  
     
    Export citation  
  7. 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.score: 90.0
    Direct download  
     
    My bibliography  
     
    Export citation  
  8. 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.score: 84.0
    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)  
     
    My bibliography  
     
    Export citation  
  9. Sueli Mendes dos Santos (1972). Automatic Proofs for Theorems on Predicate Calculus. [Rio De Janeiro,Pontificia Universidade Católica Do Rio De Janeiro].score: 78.0
     
    My bibliography  
     
    Export citation  
  10. N. Shankar (1994). Metamathematics, Machines, and Gödel's Proof. Cambridge University Press.score: 77.0
    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 (...)
     
    My bibliography  
     
    Export citation  
  11. 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.score: 62.0
    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)  
     
    My bibliography  
     
    Export citation  
  12. Michael Kohlhase, Higher-Order Automated Theorem Proving.score: 56.0
    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 to English
    | Direct download  
     
    My bibliography  
     
    Export citation  
  13. Francis J. Pelletier (1993). Identity in Modal Logic Theorem Proving. Studia Logica 52 (2):291 - 308.score: 56.0
    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)  
     
    My bibliography  
     
    Export citation  
  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.score: 56.0
    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  
     
    My bibliography  
     
    Export citation  
  15. Christoph Kreitz & Brigitte Pientka (2001). Connection-Driven Inductive Theorem Proving. Studia Logica 69 (2):293-326.score: 56.0
    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)  
     
    My bibliography  
     
    Export citation  
  16. Alberto Momigliano, Theorem Proving Via Uniform Proofs>.score: 56.0
    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 (...)
    No categories
    Direct download (5 more)  
     
    My bibliography  
     
    Export citation  
  17. Gordon Beavers (1993). Automated Theorem Proving for Łukasiewicz Logics. Studia Logica 52 (2):183 - 195.score: 45.0
    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)  
     
    My bibliography  
     
    Export citation  
  18. 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.score: 45.0
     
    My bibliography  
     
    Export citation  
  19. Bernhard Beckert & Rajeev GorÉ (2001). Free-Variable Tableaux for Propositional Modal Logics. Studia Logica 69 (1):59-96.score: 42.0
    Free-variable semantic tableaux are a well-established technique for first-order theorem proving where free variables act as a meta-linguistic device for tracking the eigenvariables used during proof search. We present the theoretical foundations to extend this technique to propositional modal logics, including non-trivial rigorous proofs of soundness and completeness, and also present various techniques that improve the efficiency of the basic naive method for such tableaux.
    Direct download (7 more)  
     
    My bibliography  
     
    Export citation  
  20. Mateja Jamnik, Alan Bundy & Ian Green (1999). On Automating Diagrammatic Proofs of Arithmetic Arguments. Journal of Logic, Language and Information 8 (3):297-321.score: 42.0
    Theorems in automated theorem proving are usually proved by formal logical proofs. However, there is a subset of problems which humans can prove by the use of geometric operations on diagrams, so called diagrammatic proofs. Insight is often more clearly perceived in these proofs than in the corresponding algebraic proofs; they capture an intuitive notion of truthfulness that humans find easy to see and understand. We are investigating and automating such diagrammatic reasoning about mathematical theorems. Concrete, rather than (...)
    Direct download (5 more)  
     
    My bibliography  
     
    Export citation  
  21. Christoph Benzmüller (2002). Comparing Approaches to Resolution Based Higher-Order Theorem Proving. Synthese 133 (1-2):203 - 235.score: 42.0
    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)  
     
    My bibliography  
     
    Export citation  
  22. 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.score: 42.0
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  23. Ewa Orłowska (1969). Mechanical Theorem Proving in a Certain Class of Formulae of the Predicate Calculus. Studia Logica 25 (1):17 - 29.score: 42.0
  24. Jan van Eijck, HyLoTab — Tableau-Based Theorem Proving for Hybrid Logics.score: 42.0
    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].
    No categories
    Translate to English
    | Direct download  
     
    My bibliography  
     
    Export citation  
  25. David C. Cooper (1970). Review: James R. Slagle, Philip Bursky, Experiments with a Multipurpose, Theorem-Proving Heuristic Program. [REVIEW] Journal of Symbolic Logic 35 (4):596-596.score: 42.0
    Direct download (2 more)  
     
    My bibliography  
     
    Export citation  
  26. Gerhard Jager & Structural Rules Residuation (2004). Alexander Koller, Ralph Debusmann, Malte Gabsdil, and Kristina Striegnitz/Put My Galakmid Coin Into the Dispenser and Kick It: Computational Linguistics and Theorem Proving in a Computer Game 187–206. Journal of Logic, Language and Information 13:537-539.score: 42.0
    No categories
    Direct download  
     
    My bibliography  
     
    Export citation  
  27. Jeremy George Peterson (1978). An Automatic Theorem Prover for Substitution and Detachment Systems. Notre Dame Journal of Formal Logic 19 (1):119-122.score: 42.0
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  28. David Luckham (1966). Review: J. A. Robinson, Theorem-Proving on the Computer. [REVIEW] Journal of Symbolic Logic 31 (3):514-515.score: 42.0
    Direct download (2 more)  
     
    My bibliography  
     
    Export citation  
  29. Bernard Meltzer (1968). Some Recent Developments in Complete Strategies for Theorem-Proving by Computer. Zeitschrift für Mathematische Logik Und Grundlagen der Mathematik 14 (25-29):377-382.score: 42.0
    No categories
    Direct download (2 more)  
     
    My bibliography  
     
    Export citation  
  30. Anita Wasilewska (1985). Some Remarks on Theorem Proving Systems and Mazurkiewicz Algorithms Associated with Them. Mathematical Logic Quarterly 31 (19‐20):289-294.score: 42.0
    No categories
    Direct download (6 more)  
     
    My bibliography  
     
    Export citation  
  31. Gabriel Aguilera, Inma P. de Guzmán & Manuel Ojeda (1995). Increasing the Efficiency of Automated Theorem Proving. Journal of Applied Non-Classical Logics 5 (1):9-29.score: 42.0
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  32. P. Braffort & F. van Scheepen (eds.) (1968). Automation in Language Translation and Theorem Proving. Brussels, Commission of the European Communities, Directorate-General for Dissemination of Information.score: 42.0
    No categories
     
    My bibliography  
     
    Export citation  
  33. Alfredo Ferro (1993). Review: Melvin Fitting, First-Order Logic and Automated Theorem Proving. [REVIEW] Journal of Symbolic Logic 58 (2):719-719.score: 42.0
    Direct download (2 more)  
     
    My bibliography  
     
    Export citation  
  34. Jean Flower, Judith Masthoff & Gem Stapleton (2004). Generating Readable Proofs: A Heuristic Approach to Theorem Proving with Spider Diagrams. In. In A. Blackwell, K. Marriott & A. Shimojima (eds.), Diagrammatic Representation and Inference. Springer. 166--181.score: 42.0
    No categories
    Direct download (2 more)  
     
    My bibliography  
     
    Export citation  
  35. Eric Livingston (2005). Natural Reasoning in Mathematical Theorem Proving. Communication and Cognition. Monographies 38 (3-4):319-344.score: 42.0
    No categories
     
    My bibliography  
     
    Export citation  
  36. David Luckham (1996). Robinson JA. Theorem-Proving on the Computer. Journal of the Association for Computing Machinery, Vol. 10 (1963), Pp. 163–174. [REVIEW] Journal of Symbolic Logic 31 (3):514-515.score: 42.0
    Direct download  
     
    My bibliography  
     
    Export citation  
  37. David Luckham (1967). Review: Lawrence Wos, George A. Robinson, Daniel F. Carson, Efficiency and Completeness of the Set of Support Strategy in Theorem Proving. [REVIEW] Journal of Symbolic Logic 32 (1):117-118.score: 42.0
    Direct download  
     
    My bibliography  
     
    Export citation  
  38. David Luckham (1967). Review: Lawrence Wos, Daniel Carson, George Robinson, The Unit Preference Strategy in Theorem Proving. [REVIEW] Journal of Symbolic Logic 32 (1):117-117.score: 42.0
    Direct download (2 more)  
     
    My bibliography  
     
    Export citation  
  39. Mi Lu & Jinzhao Wu (2000). On Theorem Proving in Annotated Logics. Journal of Applied Non-Classical Logics 10 (2):121-143.score: 42.0
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  40. 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.score: 42.0
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  41. E. Orlowska (1985). Mechanical Theorem Proving for Post Logics. Logique Et Analyse 110:173-192.score: 42.0
     
    My bibliography  
     
    Export citation  
  42. Francis Jeffry Pelletier (1998). Natural Deduction Theorem Proving in THINKER. Studia Logica 60 (1):3-43.score: 42.0
     
    My bibliography  
     
    Export citation  
  43. Uwe Petermann (2014). Theorem Proving with Built-in Hybrid Theories. Logic and Logical Philosophy 6:77.score: 42.0
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  44. J. A. Robinson (1980). Review: Donald W. Loveland, Automated Theorem Proving. A Logical Basis. [REVIEW] Journal of Symbolic Logic 45 (3):629-630.score: 42.0
    Direct download (2 more)  
     
    My bibliography  
     
    Export citation  
  45. J. A. Robinson (1967). Review: H. Gelernter, Theorem Proving by Machine; H. Gelernter, Realization of a Geometry Theorem Proving Machine. [REVIEW] Journal of Symbolic Logic 32 (4):522-523.score: 42.0
    Direct download  
     
    My bibliography  
     
    Export citation  
  46. J. A. Robinson (1967). Review: Martin Davis, George Logemann, Donald Loveland, A Machine Program for Theorem-Proving. [REVIEW] Journal of Symbolic Logic 32 (1):118-118.score: 42.0
    Direct download  
     
    My bibliography  
     
    Export citation  
  47. T. Gergely & K. P. Vershinin (1978). Model Theoretical Investigation of Theorem Proving Methods. Notre Dame Journal of Formal Logic 19 (4):523-542.score: 42.0
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  48. Tomás E. Uribe (2000). Combinations of Model Checking and Theorem Proving. In. In Dov M. Gabbay & Maarten de Rijke (eds.), Frontiers of Combining Systems. Research Studies Press. 151--170.score: 42.0
    No categories
    Direct download (2 more)  
     
    My bibliography  
     
    Export citation  
  49. Joyce Friedman (1967). Review: B. Dunham, R. Fridshal, G. L. Sward, A Non-Heuristic Program for Proving Elementary Logical Theorems; B. Dunham, R. Fridshal, J. H. North, Exploratory Mathematics by Machine; B. Dunham, J. H. North, Theorem Testing by Computer. [REVIEW] Journal of Symbolic Logic 32 (2):266-266.score: 36.0
    Direct download (2 more)  
     
    My bibliography  
     
    Export citation  
  50. J. A. Robinson (1967). Review: Abraham Robinson, Proving a Theorem (as Done by Man, Logician, or Machine). [REVIEW] Journal of Symbolic Logic 32 (4):522-522.score: 36.0
    Direct download (2 more)  
     
    My bibliography  
     
    Export citation  
1 — 50 / 1000