Found 20 Documents (Results 1–20)
Analogy in automated deduction: a survey. (English) Zbl 1341.68183
Prade, Henri (ed.) et al., Computational approaches to analogical reasoning: current trends. Revised and extended versions of papers based on the presentations at the international workshop on similarity and analogy-based methods in AI, SAMAI ’12, co-located with the 20th European conference on artificial intelligence, ECAI ’12, Montpellier, France, August 27, 2012. Berlin: Springer (ISBN 978-3-642-54515-3/hbk; 978-3-642-54516-0/ebook). Studies in Computational Intelligence 548, 103-130 (2014).
MSC:
68T15
03B35
Crystal: Integrating structured queries into a tactic language. (English) Zbl 1185.68618
MSC:
68T15
68N15
Supporting the formal verification of mathematical texts. (English) Zbl 1107.68104
MSC:
68T15
03B35
Computer supported mathematics with \(\Omega\)MEGA. (English) Zbl 1107.68101
MSC:
68T15
68W30
A proof-centric approach to mathematical assistants. (English) Zbl 1107.68096
MSC:
68T15
Theorema: Towards computer-aided mathematical theory exploration. (English) Zbl 1107.68095
MSC:
68T15
13P10
Computer theorem proving in mathematics. (English) Zbl 1067.03020
Reviewer: Alfredo Burrieza Muñiz (Málaga)
A formalisation of weak normalisation (with respect to permutations) of sequent calculus proofs. (English) Zbl 0951.03049
Knowledge-based proof planning. (English) Zbl 0939.68822
MSC:
68T15
Higher-order annotated terms for proof search. (English) Zbl 1543.68412
von Wright, J. (ed.) et al., Theorem proving in higher order logics. 9th international conference, TPHOL ’96, Turku, Finland, August 26–30, 1996. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 1125, 399-413 (1996).
Using tactics to reformulate formulae for resolution theorem proving. (English) Zbl 0891.68094
MSC:
68T15
Mollusc: a general proof-development shell for sequent-based logics. (English) Zbl 1433.68564
Bundy, Alan (ed.), Automated deduction – CADE-12. 12th international conference, Nancy, France, June 26 – July 1, 1994. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 814, 826-830 (1994).
MSC:
68V15
Reconstructing proofs at the assertion level. (English) Zbl 1433.68551
Bundy, Alan (ed.), Automated deduction – CADE-12. 12th international conference, Nancy, France, June 26 – July 1, 1994. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 814, 738-752 (1994).
MSC:
68V15
Lazy techniques for fully expansive theorem proving. (English) Zbl 0785.68077
MSC:
68T15
Rippling: A heuristic for guiding inductive proofs. (English) Zbl 0789.68121
Reviewer: A.Leitsch (Wien)
MSC:
68T15
03B35
Experiments with proof plans for induction. (English) Zbl 0733.68069
MSC:
68T15
68T20
Extensions to the rippling-out tactic for guiding inductive proofs. (English) Zbl 1509.68300
Stickel, Mark E. (ed.), Automated deduction – CADE-10. 10th international conference, Kaiserslautern, Germany, July 24–27, 1990. Proceedings. Berlin etc.: Springer-Verlag. Lect. Notes Comput. Sci. 449, 132-146 (1990).
Filter Results by …
Document Type
- Journal Articles (15)
- Collection Articles (5)
all
top 5
Author
- Smaill, Alan (5)
- Bundy, Alan (3)
- van Harmelen, Frank (3)
- Ireland, Andrew (2)
- Siekmann, Jörg H. (2)
- Adams, Andrew A. (1)
- Autexier, Serge (1)
- Benzmüller, Christoph Ewald (1)
- Boulton, Richard J. (1)
- Boy de la Tour, Thierry (1)
- Buchberger, Bruno (1)
- Buss, Samuel R. (1)
- Crǎciun, Adrian (1)
- Dietrich, Dominik (1)
- Dixon, Lucas (1)
- Fleuriot, Jacques D. (1)
- Galmiche, Didier (1)
- Green, Ian (1)
- Hesketh, Jane (1)
- Huang, Xiaorong (1)
- Iemhoff, Rosalie (1)
- Jebelean, Tudor (1)
- Kerber, Manfred (1)
- Kohlenbach, Ulrich Wilhelm (1)
- Korukhova, Yulia (1)
- Kovács, Laura Ildikó (1)
- Kraan, Ina (1)
- Kutsia, Temur (1)
- Melis, Erica (1)
- Nakagawa, Koji (1)
- Peltier, Nicolas (1)
- Piroi, Florina (1)
- Popov, Nikolaj (1)
- Präcklein, Axel (1)
- Pym, David J. (1)
- Rathjen, Michael (1)
- Richards, Bradley L. (1)
- Robu, Judit (1)
- Rosenkranz, Markus (1)
- Schulz, Ewaryst (1)
- Simpson, Carlos Tschudi (1)
- Stevens, Andrew (1)
- Wiggins, Geraint A. (1)
- Windsteiger, Wolfgang (1)
- Zinn, Claus (1)
all
top 5
Serial
- J. Appl. Log. (4)
- Artif. Intell. (2)
- J. Autom. Reasoning (2)
- Ann. Math. Artif. Intell. (2)
- Lett. Math. Phys. (1)
- Theor. Comput. Sci. (1)
- Form. Methods Syst. Des. (1)
- LMS J. Comput. Math. (1)
- Oberwolfach Rep. (1)
all
top 3
Software
- Nuprl (20)
- CLAM (9)
- Oyster (9)
- Coq (8)
- Isabelle (7)
- LCF (5)
- Automath (4)
- HOL (4)
- Isar (4)
- Lambda-Clam (4)
- Mizar (4)
- OTTER (4)
- SPASS (4)
- TPS (4)
- Bliksem (3)
- Isabelle/HOL (3)
- ML (3)
- PVS (3)
- Waldmeister (3)
- HOL Light (2)
- IsaPlanner (2)
- LEGO (2)
- LOUI (2)
- MAYA (2)
- Omega-MKRP (2)
- PROTEIN (2)
- Proof General (2)
- SETHEO (2)
- TPTP (2)
- TeXmacs (2)
- Theorema (2)
- XBarnacle (2)
- ACL2 (1)
- ALISA (1)
- APS-1 (1)
- ActiveMath (1)
- Analytica (1)
- Archive Formal Proofs (1)
- CASL (1)
- Cambridge LCF (1)
- E Theorem Prover (1)
- EQP (1)
- ETPS (1)
- Elf (1)
- Flyspeck (1)
- GAP (1)
- IMPS (1)
- IsaWin (1)
- Isabelle/Isar (1)
- Jape (1)
- Leo (1)
- Lolli (1)
- MBase (1)
- MKRP (1)
- MML (1)
- MathWeb (1)
- Mathematica (1)
- Matita (1)
- Minlog (1)
- MoMM (1)
- Mollusc (1)
- Multi (1)
- NQTHM (1)
- OMDoc (1)
- Omega-ANTS (1)
- P.rex (1)
- Pesca (1)
- PhoX (1)
- Prodigy (1)
- SATCHMO (1)
- SKIL (1)
- Stratego (1)
- TAS (1)
- TRAMP (1)
- VAMPIRE (1)
- Whelp (1)
- Z (1)
- cubicaltt (1)
- fastZeil (1)