Document Search Results

Newest Citations Relevance

Nummelin, Visa; Bentkamp, Alexander; Tourret, Sophie; Vukmirović, Petar

Superposition with first-class Booleans and inprocessing clausification. (English) Zbl 1540.03025

Platzer, André (ed.) et al., Automated deduction – CADE 28. 28th international conference on automated deduction, virtual event, July 12–15, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12699, 378-395 (2021).

MSC: 03B35 68V15

Cite Review PDF

Full Text: DOI

OA License

Cauderlier, Raphaël

Tactics and certificates in Meta Dedukti. (English) Zbl 1482.68266

Avigad, Jeremy (ed.) et al., Interactive theorem proving. 9th international conference, ITP 2018, held as part of the federated logic conference, FloC 2018, Oxford, UK, July 9–12, 2018. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 10895, 142-159 (2018).

MSC: 68V15 03B70

Cite Review PDF

Full Text: DOI

Reynolds, Andrew; King, Tim; Kuncak, Viktor

Solving quantified linear arithmetic by counterexample-guided instantiation. (English) Zbl 1377.68138

Form. Methods Syst. Des. 51, No. 3, 500-532 (2017).

MSC: 68Q60 03B70 68T15

Cite Review PDF

Full Text: DOI Link

Reger, Giles; Suda, Martin; Voronkov, Andrei

Finding finite models in multi-sorted first-order logic. (English) Zbl 1475.68447

Creignou, Nadia (ed.) et al., Theory and applications of satisfiability testing – SAT 2016. 19th international conference, Bordeaux, France, July 5–8, 2016. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9710, 323-341 (2016).

MSC: 68V15 03C13 68T20

Cite Review PDF

Full Text: DOI arXiv

Blanchette, Jasmin Christian; Böhme, Sascha; Fleury, Mathias; Smolka, Steffen Juilf; Steckermeier, Albert

Semi-intelligible Isar proofs from machine-generated proofs. (English) Zbl 1356.68178

J. Autom. Reasoning 56, No. 2, 155-200 (2016).

MSC: 68T15 03B35

Cite Review PDF

Full Text: DOI HAL

Echenim, Mnacho; Peltier, Nicolas; Tourret, Sophie

Quantifier-free equational logic and prime implicate generation. (English) Zbl 1465.68280

Felty, Amy P. (ed.) et al., Automated deduction – CADE-25. 25th international conference on automated deduction, Berlin, Germany, August 1–7, 2015. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9195, 311-325 (2015).

MSC: 68V15 03B35

Cite Review PDF

Full Text: DOI

Hetzl, Stefan; Leitsch, Alexander; Reis, Giselle; Weller, Daniel

Algorithmic introduction of quantified cuts. (English) Zbl 1393.03050

Theor. Comput. Sci. 549, 1-16 (2014).

MSC: 03F05

Cite Review PDF

Full Text: DOI arXiv

Sutcliffe, Geoff; Schulz, Stephan; Claessen, Koen; Baumgartner, Peter

The TPTP typed first-order form with arithmetic. (English) Zbl 1352.68217

Bjørner, Nikolaj (ed.) et al., Logic for programming, artificial intelligence, and reasoning. 18th international conference, LPAR-18, Mérida, Venezuela, March 11–15, 2012. Proceedings. Berlin: Springer (ISBN 978-3-642-28716-9/pbk). Lecture Notes in Computer Science 7180, 406-419 (2012).

MSC: 68T15 03B35

Cite Review PDF

Full Text: DOI

Ge, Yeting; Barrett, Clark; Tinelli, Cesare

Solving quantified verification conditions using satisfiability modulo theories. (English) Zbl 1184.68461

Ann. Math. Artif. Intell. 55, No. 1-2, 101-122 (2009).

MSC: 68T15 03B35 68T20

Cite Review PDF

Full Text: DOI

Bongio, Jeremy; Katrak, Cyrus; Lin, Hai; Lynch, Christopher; McGgregor, Ralph Eric

Encoding first order proofs in SMT. (English) Zbl 1277.03006

Krstić, Sava (ed.) et al., Proceedings of the 5th international workshop on satisfiability modulo theories (SMT 2007), Berlin, Germany, July 1–2, 2007. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 198, No. 2, 71-84 (2008).

MSC: 03B35 68T15

Cite Review PDF

Full Text: DOI

Found 10 Documents (Results 1–10)

Superposition with first-class Booleans and inprocessing clausification. (English) Zbl 1540.03025

Tactics and certificates in Meta Dedukti. (English) Zbl 1482.68266

Solving quantified linear arithmetic by counterexample-guided instantiation. (English) Zbl 1377.68138

Finding finite models in multi-sorted first-order logic. (English) Zbl 1475.68447

Semi-intelligible Isar proofs from machine-generated proofs. (English) Zbl 1356.68178

Quantifier-free equational logic and prime implicate generation. (English) Zbl 1465.68280

Algorithmic introduction of quantified cuts. (English) Zbl 1393.03050

The TPTP typed first-order form with arithmetic. (English) Zbl 1352.68217

Solving quantified verification conditions using satisfiability modulo theories. (English) Zbl 1184.68461

Encoding first order proofs in SMT. (English) Zbl 1277.03006

Filter Results by …

Document Type

Author

Serial

Year of Publication

Main Field

Software