Document Search Results

Newest Citations Relevance

Definitional quantifiers realise semantic reasoning for proof by induction. (English) Zbl 1514.68311

Kovács, Laura (ed.) et al., Tests and proofs. 16th international conference, TAP 2022, held as part of STAF 2022, Nantes, France, July 5, 2022. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 13361, 48-66 (2022).

MSC: 68V15

Cite Review PDF

Full Text: DOI arXiv

Shimoda, Takumi; Kobayashi, Naoki; Sakayori, Ken; Sato, Ryosuke

Symbolic automatic relations and their applications to SMT and CHC solving. (English) Zbl 1497.68320

Drăgoi, Cezara (ed.) et al., Static analysis. 28th international symposium, SAS 2021, Chicago, IL, USA, October 17–19, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12913, 405-428 (2021).

MSC: 68Q60 68P05 68Q45 68V15

Cite Review PDF

Full Text: DOI arXiv

Gauthier, Thibault; Kaliszyk, Cezary; Urban, Josef; Kumar, Ramana; Norrish, Michael

TacticToe: learning to prove with tactics. (English) Zbl 1543.68400

J. Autom. Reasoning 65, No. 2, 257-286 (2021).

MSC: 68V15 68T20 68V20

Cite Review PDF

Full Text: DOI arXiv

De Angelis, Emanuele; Fioravanti, Fabio; Pettorossi, Alberto; Proietti, Maurizio

Removing algebraic data types from constrained Horn clauses using difference predicates. (English) Zbl 07614508

Peltier, Nicolas (ed.) et al., Automated reasoning. 10th international joint conference, IJCAR 2020, Paris, France, July 1–4, 2020. Proceedings. Part I. Cham: Springer. Lect. Notes Comput. Sci. 12166, 83-102 (2020).

MSC: 68V15

Cite Review PDF

Full Text: DOI arXiv

Lin, Yuhui; Bundy, Alan; Grov, Gudmund; Maclean, Ewen

Automating Event-B invariant proofs by rippling and proof patching. (English) Zbl 1425.68077

Formal Asp. Comput. 31, No. 1, 95-129 (2019).

MSC: 68N30 68Q60 68T15

Cite Review PDF

Full Text: DOI

OA License

Drămnesc, Isabela; Jebelean, Tudor; Stratulat, Sorin

Mechanical synthesis of sorting algorithms for binary trees by logic and combinatorial techniques. (English) Zbl 1395.68246

J. Symb. Comput. 90, 3-41 (2019).

MSC: 68T15 68P10

Cite Review PDF

Full Text: DOI HAL

Jiang, Yaqing; Papapanagiotou, Petros; Fleuriot, Jacques

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).

MSC: 68V15 68T05

Cite Review PDF

Full Text: DOI Link

Lin, Yuhui; Grov, Gudmund; Arthan, Rob

Understanding and maintaining tactics graphically OR how we are learning that a diagram can be worth more than 10K LoC. (English) Zbl 1451.68324

J. Formaliz. Reason. 9, No. 2, 69-130 (2016).

MSC: 68V15 68N18

Cite Review PDF

Full Text: DOI arXiv

Gransden, Thomas; Walkinshaw, Neil; Raman, Rajeev

Mining state-based models from proof corpora. (English) Zbl 1304.68155

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, 282-297 (2014).

MSC: 68T15

Cite Review PDF

Full Text: DOI arXiv Link

Johansson, Moa; Rosén, Dan; Smallbone, Nicholas; Claessen, Koen

Hipster: integrating theory exploration in a proof assistant. (English) Zbl 1304.68157

MSC: 68T15

Cite Review PDF

Full Text: DOI arXiv

Johansson, Moa; Dixon, Lucas; Bundy, Alan

Conjecture synthesis for inductive theories. (English) Zbl 1243.68268

J. Autom. Reasoning 47, No. 3, 251-289 (2011).

MSC: 68T15

Cite Review PDF

Full Text: DOI Link

Brotherston, James; Distefano, Dino; Petersen, Rasmus Lerchedahl

Automated cyclic entailment proofs in separation logic. (English) Zbl 1341.68184

Bjørner, Nikolaj (ed.) et al., Automated deduction – CADE-23. 23rd international conference on automated deduction, Wrocław, Poland, July 31 – August 5, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-22437-9/pbk; 978-3-642-22438-6/ebook). Lecture Notes in Computer Science 6803. Lecture Notes in Artificial Intelligence, 131-146 (2011).

MSC: 68T15 03B70

Cite Review PDF

Full Text: DOI

Dennis, Louise Abigail; Green, Ian; Smaill, Alan

The use of embeddings to provide a clean separation of term and annotation for higher order rippling. (English) Zbl 1216.68232

J. Autom. Reasoning 47, No. 1, 57-105 (2011).

MSC: 68T15

Cite Review PDF

Full Text: DOI

Johansson, Moa; Dixon, Lucas; Bundy, Alan

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

Cite Review PDF

Full Text: DOI Link

Melis, Erica; Meier, Andreas; Siekmann, Jörg

Proof planning with multiple strategies. (English) Zbl 1182.68259

Artif. Intell. 172, No. 6-7, 656-684 (2008).

MSC: 68T20 68T15

Cite Review PDF

Full Text: DOI

Zinn, Claus

Supporting the formal verification of mathematical texts. (English) Zbl 1107.68104

J. Appl. Log. 4, No. 4, 592-621 (2006).

MSC: 68T15 03B35

Cite Review PDF

Full Text: DOI

Dixon, Lucas; Fleuriot, Jacques

A proof-centric approach to mathematical assistants. (English) Zbl 1107.68096

J. Appl. Log. 4, No. 4, 505-532 (2006).

MSC: 68T15

Cite Review PDF

Full Text: DOI Link

Found 17 Documents (Results 1–17)

Definitional quantifiers realise semantic reasoning for proof by induction. (English) Zbl 1514.68311

Symbolic automatic relations and their applications to SMT and CHC solving. (English) Zbl 1497.68320

TacticToe: learning to prove with tactics. (English) Zbl 1543.68400

Removing algebraic data types from constrained Horn clauses using difference predicates. (English) Zbl 07614508

Automating Event-B invariant proofs by rippling and proof patching. (English) Zbl 1425.68077

Mechanical synthesis of sorting algorithms for binary trees by logic and combinatorial techniques. (English) Zbl 1395.68246

Machine learning for inductive theorem proving. (English) Zbl 1515.68344

Understanding and maintaining tactics graphically OR how we are learning that a diagram can be worth more than 10K LoC. (English) Zbl 1451.68324

Mining state-based models from proof corpora. (English) Zbl 1304.68155

Hipster: integrating theory exploration in a proof assistant. (English) Zbl 1304.68157

Conjecture synthesis for inductive theories. (English) Zbl 1243.68268

Automated cyclic entailment proofs in separation logic. (English) Zbl 1341.68184

The use of embeddings to provide a clean separation of term and annotation for higher order rippling. (English) Zbl 1216.68232

Dynamic rippling, middle-out reasoning and lemma discovery. (English) Zbl 1309.68169

Proof planning with multiple strategies. (English) Zbl 1182.68259

Supporting the formal verification of mathematical texts. (English) Zbl 1107.68104

A proof-centric approach to mathematical assistants. (English) Zbl 1107.68096

Filter Results by …

Document Type

Author

Serial

Year of Publication

Main Field

Software