Found 18 Documents (Results 1–18)
Theory exploration powered by deductive synthesis. (English) Zbl 1493.68388
Silva, Alexandra (ed.) et al., Computer aided verification. 33rd international conference, CAV 2021, virtual event, July 20–23, 2021. Proceedings. Part II. Cham: Springer. Lect. Notes Comput. Sci. 12760, 125-148 (2021).
Mechanical synthesis of sorting algorithms for binary trees by logic and combinatorial techniques. (English) Zbl 1395.68246
MSC:
68T15
68P10
Machine learning for inductive theorem proving. (English) Zbl 1515.68344
Fleuriot, Jacques (ed.) et al., Artificial intelligence and symbolic computation. 13th international conference, AISC 2018, Suzhou, China, September 16–19, 2018. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 11110, 87-103 (2018).
Into the infinite – theory exploration for coinduction. (English) Zbl 1515.68343
Fleuriot, Jacques (ed.) et al., Artificial intelligence and symbolic computation. 13th international conference, AISC 2018, Suzhou, China, September 16–19, 2018. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 11110, 70-86 (2018).
Equivalence checking of two functional programs using inductive theorem provers. (English) Zbl 1419.68038
MSC:
68N18
68T15
Quick specifications for the busy programmer. (English) Zbl 1418.68037
MSC:
68N18
Proof mining with dependent types. (English) Zbl 1367.68251
Geuvers, Herman (ed.) et al., Intelligent computer mathematics. 10th international conference, CICM 2017, Edinburgh, UK, July 17–21, 2017. Proceedings. Cham: Springer (ISBN 978-3-319-62074-9/pbk; 978-3-319-62075-6/ebook). Lecture Notes in Computer Science 10383. Lecture Notes in Artificial Intelligence, 303-318 (2017).
MSC:
68T15
68T05
Recycling proof patterns in Coq: case studies. (English) Zbl 1302.68243
MSC:
68T15
68T05
Algorithmic introduction of quantified cuts. (English) Zbl 1393.03050
MSC:
03F05
Hipster: integrating theory exploration in a proof assistant. (English) Zbl 1304.68157
Watt, Stephen M. (ed.) et al., Intelligent computer mathematics. International conference, CICM 2014, Coimbra, Portugal, July 7–11, 2014. Proceedings. Berlin: Springer (ISBN 978-3-319-08433-6/pbk). Lecture Notes in Computer Science 8543. Lecture Notes in Artificial Intelligence, 108-122 (2014).
MSC:
68T15
Conjecture synthesis for inductive theories. (English) Zbl 1243.68268
MSC:
68T15
Dynamic rippling, middle-out reasoning and lemma discovery. (English) Zbl 1309.68169
Siegler, Simon (ed.) et al., Verification, induction, termination analysis. Festschrift for Christoph Walther on the occasion of his 60th birthday. Berlin: Springer (ISBN 978-3-642-17171-0/pbk). Lecture Notes in Computer Science 6463. Lecture Notes in Artificial Intelligence, 102-116 (2010).
MSC:
68T15
Filter Results by …
Document Type
- Journal Articles (12)
- Collection Articles (6)
all
top 5
Author
- Johansson, Moa (5)
- Hetzl, Stefan (4)
- Bundy, Alan (3)
- Claessen, Koen (2)
- Dixon, Lucas (2)
- Heras, Jónathan (2)
- Komendantskaya, Ekaterina (2)
- Leitsch, Alexander (2)
- Maclean, Ewen (2)
- Reis, Giselle (2)
- Smallbone, Nicholas (2)
- Weller, Daniel S. (2)
- Algehed, Maximilian (1)
- Åman Pohjola, Johannes (1)
- Confalonieri, Roberto (1)
- Demba, Moussa (1)
- Drămnesc, Isabela (1)
- Eberhard, Sebastian (1)
- Ebner, Gabriel (1)
- Echenim, Mnacho (1)
- Einarsdóttir, Sólrún Halla (1)
- Eppe, Manfred (1)
- Fleuriot, Jacques D. (1)
- Grov, Gudmund (1)
- Itzhaky, Shachar (1)
- Jebelean, Tudor (1)
- Jiang, Yaqing (1)
- Kühnberger, Kai-Uwe (1)
- Kutz, Oliver (1)
- Lin, Yuhui (1)
- Papapanagiotou, Petros (1)
- Peltier, Nicolas (1)
- Plaza, Enric (1)
- Rosen, Dan (1)
- Schorlemmer, Marco (1)
- Singher, Eytan (1)
- Stratulat, Sorin (1)
- Vierling, Jannik (1)
all
top 5
Serial
- J. Autom. Reasoning (3)
- Ann. Pure Appl. Logic (2)
- Artif. Intell. (1)
- Inf. Process. Lett. (1)
- Theor. Comput. Sci. (1)
- J. Symb. Comput. (1)
- Formal Asp. Comput. (1)
- J. Funct. Program. (1)
- Math. Comput. Sci. (1)
all
top 3
Software
- IsaCoSy (18)
- HipSpec (10)
- Isabelle/HOL (8)
- Hipster (6)
- IsaPlanner (6)
- Theorema (6)
- Coq (5)
- Isabelle (5)
- HR (4)
- TPTP (4)
- VAMPIRE (4)
- CVC4 (3)
- Cyclist (3)
- MaSh (3)
- QuickCheck (3)
- Sledgehammer (3)
- ACL2 (2)
- AVATAR (2)
- Coq/SSReflect (2)
- E Theorem Prover (2)
- Flyspeck (2)
- MATHsAiD (2)
- ML4PG (2)
- PRMLT (2)
- QuickSpec (2)
- WEKA (2)
- z3 (2)
- Agda (1)
- Archive Formal Proofs (1)
- BliStr (1)
- CASL (1)
- CIRC (1)
- Clingo (1)
- Coinductive (1)
- CoqHammer (1)
- Dafny (1)
- Daikon (1)
- Easychair (1)
- Fiat (1)
- FlashMeta (1)
- GAPT (1)
- GitHub (1)
- HOL Light (1)
- HOLyHammer (1)
- Haskell (1)
- Hets (1)
- InKa (1)
- Leon (1)
- Mace4 (1)
- Mathematica (1)
- Matita (1)
- Matlab (1)
- Metis_ (1)
- MiniMaxSat (1)
- Mizar (1)
- NQTHM (1)
- Proof General (1)
- ProofPower (1)
- Prover9 (1)
- Rodin (1)
- SEPIA (1)
- SIMPLIFY (1)
- SMT-LIB (1)
- SPASS (1)
- SPIKE (1)
- TRANSIT (1)
- TacticToe (1)
- Whelp (1)
- Z (1)
- Zeno (1)
- egg (1)
