Document Search Results

Newest Citations Relevance

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

Leino, K. Rustan M.

Automating induction with an SMT solver. (English) Zbl 1326.68262

Kuncak, Viktor (ed.) et al., Verification, model checking, and abstract interpretation. 13th international conference, VMCAI 2012, Philadelphia, PA, USA, January 22–24, 2012. Proceedings. Berlin: Springer (ISBN 978-3-642-27939-3/pbk). Lecture Notes in Computer Science 7148, 315-331 (2012).

MSC: 68T15 68Q42 68Q60

Cite Review PDF

Full Text: DOI

van Weerdenburg, Muck

Automating soundness proofs. (English) Zbl 1339.68160

Hennessy, Matthew (ed.) et al., Proceedings of the 5th workshop on structural operational semantics (SOS 2008), Reykjavik, Iceland, July 6, 2008. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 229, No. 4, 107-118 (2009).

MSC: 68Q55 68N30 68T15

Cite Review PDF

Full Text: DOI

Siekmann, Jörg; Benzmüller, Christoph; Autexier, Serge

Computer supported mathematics with \(\Omega\)MEGA. (English) Zbl 1107.68101

J. Appl. Log. 4, No. 4, 533-559 (2006).

MSC: 68T15 68W30

Cite Review PDF

Full Text: DOI

Simpson, Carlos

Computer theorem proving in mathematics. (English) Zbl 1067.03020

Lett. Math. Phys. 69, Spec. Iss., 287-315 (2004).

Reviewer: Alfredo Burrieza Muñiz (Málaga)

MSC: 03B35 68T15 68-02

Cite Review PDF

Full Text: DOI arXiv

Hutter, Dieter

Deduction as an engineering science. (English) Zbl 1261.68102

Dahn, Ingo (ed.) et al., FTP’2003: 4th international workshop on first-order theorem proving. Proceedings of the workshop (in connection with RDP’03, federated conference on rewriting, deduction and programming), Valencia, Spain, June 12–14, 2003. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 86, No. 1, 1-8 (2003).

MSC: 68T15

Cite Review PDF

Full Text: DOI

Stratulat, Sorin

A general framework to build contextual cover set induction provers. (English) Zbl 0981.68147

J. Symb. Comput. 32, No. 4, 403-445 (2001).

MSC: 68T15 03B35

Cite Review PDF

Full Text: DOI

Mantel, Heiko; Gärtner, Felix C.

A case study in the mechanical verification of fault tolerance. (English) Zbl 1010.68170

J. Exp. Theor. Artif. Intell. 12, No. 4, 473-487 (2000).

MSC: 68T15

Cite Review PDF

Full Text: DOI

Galmiche, Didier; Pym, David J.

Proof-search in type-theoretic languages: An introduction. (English) Zbl 0952.03006

Theor. Comput. Sci. 232, No. 1-2, 5-53 (2000).

MSC: 03B35 03B15 03F03 68N18 03B70

Cite Review PDF

Full Text: DOI

Slind, Konrad

Function definition in higher-order logic. (English) Zbl 1543.68411

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, 381-397 (1996).

MSC: 68V15 03B35

Cite Review PDF

Full Text: DOI

Found 10 Documents (Results 1–10)

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

Automating induction with an SMT solver. (English) Zbl 1326.68262

Automating soundness proofs. (English) Zbl 1339.68160

Computer supported mathematics with \(\Omega\)MEGA. (English) Zbl 1107.68101

Computer theorem proving in mathematics. (English) Zbl 1067.03020

Deduction as an engineering science. (English) Zbl 1261.68102

A general framework to build contextual cover set induction provers. (English) Zbl 0981.68147

A case study in the mechanical verification of fault tolerance. (English) Zbl 1010.68170

Proof-search in type-theoretic languages: An introduction. (English) Zbl 0952.03006

Function definition in higher-order logic. (English) Zbl 1543.68411

Filter Results by …

Document Type

Author

Serial

Year of Publication

Main Field

Software