TPS: A hybrid automatic-interactive system for developing proofs

Andrews Andrews, 1996, TPS: A theorem proving system for classical type theory, J. Automat. Reason., 16, 321, 10.1007/BF00252180 Andrews, 2000, System description: Tps: A theorem proving system for type theory, vol. 1831, 164 Andrews, 2004, Etps: A system to help students write formal proofs, J. Automat. Reason., 32, 75, 10.1023/B:JARS.0000021871.18776.94 Miller, 1984, Expansion tree proofs and their conversion to natural deduction proofs, vol. 170, 375 Miller, 1987, A compact representation of proofs, Studia Logica, 46, 347, 10.1007/BF00370646 Andrews, 1989, On connections and higher-order logic, J. Automat. Reason., 5, 257, 10.1007/BF00248320 C.E. Brown, Set comprehension in Church's type theory, Ph.D. thesis, Department of Mathematical Sciences, Carnegie Mellon University, 2004 M. Bishop, P.B. Andrews, Selectively instantiating definitions, in: [53], pp. 365–380 M. Bishop, A breadth-first strategy for mating search, in: [54], pp. 359–373 Bishop C.E. Brown, Solving for set variables in higher-order theorem proving, in: [55], pp. 408–422 Andrews, 2001, Classical type theory, vol. 2, 965 Andrews, 2002 Bledsoe, 1993, Set-Var, J. Automat. Reason., 11, 293, 10.1007/BF00881869 Pfenning Andrews Andrews, 1971, Resolution in type theory, J. Symbolic Logic, 36, 414, 10.2307/2269949 Pfenning, 1990, Presenting intuitive deductions via symmetric simplification, vol. 449, 336 Benzmüller, 2004, Higher-order semantics and extensionality, J. Symbolic Logic, 69, 1027, 10.2178/jsl/1102022211 Huet, 1975, A unification algorithm for typed λ-calculus, Theoret. Comput. Sci., 1, 27, 10.1016/0304-3975(75)90011-0 Murray, 1993, Dissolution: Making paths vanish, J. ACM, 40, 504, 10.1145/174130.174135 Barker-Plummer, 1992, Gazing: An approach to the problem of definition and lemma use, J. Automat. Reason., 8, 311, 10.1007/BF02341853 Bledsoe, 1974, A man-machine theorem-proving system, Artificial Intelligence, 5, 51, 10.1016/0004-3702(74)90009-5 Andrews, 1981, Theorem proving via general matings, J. ACM, 28, 193, 10.1145/322248.322249 Bibel, 1987 Lee, 1992, Eliminating duplication with the hyper-linking strategy, J. Automat. Reason., 9, 25, 10.1007/BF00247825 Bryant, 1986, Graph-based algorithms for boolean function manipulation, IEEE Trans. Comput. C-35(8), 677, 10.1109/TC.1986.1676819 C. Benzmüller, Equality and extensionality in automated higher-order theorem proving, Ph.D. thesis, Universität des Saarlandes, 1999 C. Benzmüller, M. Kohlhase, System description: LEO—a higher-order theorem prover, in: [53], pp. 139–143 Konrad, 1998, HOT: A concurrent automated theorem prover based on higher-order tableaux, vol. 1479, 245 Konrad, 2004, Model Generation for Natural Language Interpretation and Analysis, vol. 2953 Gordon, 1988, HOL: A proof generating system for higher-order logic, 73 Gordon, 1993 J.R. Harrison, Theorem proving with the real numbers, Ph.D. thesis, Churchill College, Cambridge, revised version available as Technical Report TR408, Computer Laboratory, Cambridge University, 1996 Paulson, 1989, The foundation of a generic theorem prover, J. Automat. Reason., 5, 363, 10.1007/BF00248324 Paulson, 1994, Isabelle: A Generic Theorem Prover, vol. 828 Farmer, 1993, IMPS: An interactive mathematical proof system, J. Automat. Reason., 11, 213, 10.1007/BF00881906 J. Richardson, A. Smaill, I. Green, System description: Proof planning in higher-order logic with λ-Clam, in: [53], pp. 129–133 Lacey, 2000, Logic program synthesis in a higher-order setting, vol. 1861, 87 Miller, 1991, A logic programming language with lambda-abstraction, function variables, and simple unification, J. Logic Comput., 1, 497, 10.1093/logcom/1.4.497 F. Pfenning, C. Schürmann, System description: Twelf—a meta-logical framework for deductive systems, in: [54], pp. 202–206 Owre, 1996, PVS: Combining specification, proof checking, and model checking, vol. 1102, 411 Shankar, 2001, Using decision procedures with a higher-order logic, vol. 2152, 5 R.L.C. et al., Implementing Mathematics with the Nuprl Proof Development System, Prentice-Hall, 1986 Siekmann 1998, vol. 1421 1999, vol. 1632 2002, vol. 2392