
ETPS
 Referenced in 153 articles
[sw06302]
 prove theorems of first and higherorder logic interactively, automatically, or in a mixture ... into expansion proofs, and solving unification problems in higherorder logic. It has a formula...

TPS
 Referenced in 71 articles
[sw00973]
 prove theorems of first and higherorder logic interactively, automatically, or in a mixture ... into expansion proofs, and solving unification problems in higherorder logic. It has a formula...

Athena
 Referenced in 10 articles
[sw09967]
 logics, including higherorder logic. It retains the tractability of firstorder logic (completeness, compactness ... over terms and formulas, efficient matching and unification algorithms, etc.), while overcoming some...

clam3
 Referenced in 0 articles
[sw19621]
 proof planner with critics, and some higherorder unification, in the v3 branch of Clam...

NuprlLight
 Referenced in 1 article
[sw31982]
 NuprlLight: an implementation framework for higherorder logics. this paper we describe NuprlLight ... Isabelle. However, where Isabelle uses higher order unification and resolution, NuprlLight retains a tactic...

ACL2
 Referenced in 275 articles
[sw00060]
 ACL2 is both a programming language in which...

Coq
 Referenced in 1760 articles
[sw00161]
 Coq is a formal proof management system. It...

Isabelle
 Referenced in 602 articles
[sw00454]
 Isabelle is a generic proof assistant. It allows...

LAPACK
 Referenced in 1600 articles
[sw00503]
 LAPACK is written in Fortran 90 and provides...

Maple
 Referenced in 4977 articles
[sw00545]
 The result of over 30 years of cutting...

Mathematica
 Referenced in 5766 articles
[sw00554]
 Almost any workflow involves computing results, and that...

Matlab
 Referenced in 11686 articles
[sw00558]
 MATLAB® is a highlevel language and interactive...

SETHEO
 Referenced in 119 articles
[sw00707]
 SETHEO: A highperformance theorem prover. The paper...

REDUCE
 Referenced in 739 articles
[sw00789]
 REDUCE is an interactive system for general algebraic...

SUBSEXPL
 Referenced in 3 articles
[sw00923]
 We present the system SUBSEXPL used for simulating...

MACSYMA
 Referenced in 714 articles
[sw01209]
 Macsyma is a general purpose symbolicnumericalgraphical...

ML
 Referenced in 502 articles
[sw01218]
 ML (’Meta Language’) is a generalpurpose functional...

ALGOL 68
 Referenced in 285 articles
[sw01226]
 ALGOL 68 (short for ALGOrithmic Language 1968) is...

Stratego
 Referenced in 75 articles
[sw01259]
 Stratego/XT is a language and toolset for program...

Beluga
 Referenced in 25 articles
[sw01321]
 Our main interest in this project is to...