
OTTER
 Referenced in 257 articles
[sw02904]
 designed to prove theorems stated in firstorder logic with equality. Otter’s inference rules...

VAMPIRE
 Referenced in 184 articles
[sw02918]
 automatic theorem prover for firstorder classical logic. It consists of a shell ... kernel. The kernel implements the calculi of ordered binary resolution and superposition for handling equality ... ordered unit equalities, and a lightweight basicness. The CASC version uses the KnuthBendix ordering ... accepts a problem in the full firstorder logic syntax, clausifies it and performs...

E Theorem Prover
 Referenced in 141 articles
[sw10187]
 theorem prover for full firstorder logic with equality. It accepts a problem specification, typically ... consisting of a number of firstorder clauses or formulas, and a conjecture, again either ... powerful and friendly reasoning systems for firstorder logic. The prover has successfully participated...

SPASS
 Referenced in 132 articles
[sw04108]
 automated theorem prover for firstorder logic with equality. So the input for the prover ... valid and because validity in firstorder logic is undecidable, SPASS may run forever without...

ETPS
 Referenced in 142 articles
[sw06302]
 automated theoremprover for firstorder logic and type theory. The latter...

Prover9
 Referenced in 132 articles
[sw04969]
 automated theorem prover for firstorder and equational logic, and Mace4 searches for finite models...

TPS
 Referenced in 66 articles
[sw00973]
 automated theoremprover for firstorder logic and type theory. The latter...

iProver
 Referenced in 35 articles
[sw09707]
 instantiationbased theorem prover for firstorder logic. iProver is an instantiationbased theorem prover ... InstGen calculus, complete for firstorder logic. One of the distinctive features of iProver...

Ivy
 Referenced in 29 articles
[sw10279]
 Preprocessor and Proof Checker for FirstOrder Logic. This case study shows how nonACL2 ... resolution/paramodulation automated theorem proving for firstorder logic. The top ACL2 function takes a conjecture...

KeY
 Referenced in 54 articles
[sw09969]
 novel theorem prover for the firstorder Dynamic Logic for Java with a userfriendly...

GEOTHER 1.1
 Referenced in 27 articles
[sw02842]
 English or Chinese statement, into a firstorder logical formula, or into algebraic expressions; draw...

Darwin
 Referenced in 23 articles
[sw04175]
 automated theorem prover for first order clausal logic. It accepts problems formulated in tptp ... problems than propositional approaches. Darwin is the first implementation of the Model Evolution Calculus ... lifts the propositional DPLL procedure to firstorder logic. One of the main motivations ... possibility of migrating to the firstorder level some of those very effective search techniques...

leanCoP
 Referenced in 18 articles
[sw09756]
 very compact theorem prover for classical firstorder logic, based on the connection (tableau) calculus ... compact theorem prover for intuitionistic firstorder logic and based on the clausal connection calculus...

SCR
 Referenced in 17 articles
[sw06939]
 semantics by enabling events in firstorder logic via two symbols pred and succ. This ... slight extension of firstorder logic allows us to increase the readability...

REDLOG
 Referenced in 140 articles
[sw04250]
 logic system, i.e., a system that provides algorithms for the symbolic manipulation of firstorder...

KeYmaera
 Referenced in 28 articles
[sw03709]
 which is a realvalued firstorder dynamic logic for hybrid programs, a program notation...

Princess
 Referenced in 21 articles
[sw06872]
 Theorem Proving in FirstOrder Logic modulo Linear Integer Arithmetic. Princess is a theorem prover...

Hyperproof
 Referenced in 21 articles
[sw22172]
 software program. Unlike traditional treatments of firstorder logic, Hyperproof combines graphical and sentential information...

Athena
 Referenced in 10 articles
[sw09967]
 Athena is based on manysorted firstorder logic. Manysorted firstorder logic ... Maria Manzano in her ”Extensions of firstorder logic”) have argued that ... logic. It retains the tractability of firstorder logic (completeness, compactness, structural induction over terms...

ModLeanTAP
 Referenced in 17 articles
[sw12368]
 modular labelled tableau calculus for propositional modal logics (where the labels contain free and universal ... lean tableaubased prover for firstorder logic leanTAP. ModLeanTAP Version 2.0 includes additional search...