
LEOII
 Referenced in 51 articles
[sw00512]
 higherorder logic. At present LEOII can cooperate with TPTP compliant firstorder automated ... division (automation of higherorder logic) at CASCJ5. At CASC ... also participate in the firstorder divisions FOF and CNF and performed reasonably well...

ILTP
 Referenced in 26 articles
[sw00437]
 Intuitionistic Logic Theorem Proving (ILTP) library provides a platform for testing and benchmarking automated theorem ... proving (ATP) systems for firstorder and propositional intuitionistic logic. It includes two problem collections ... firstorder and propositional intuitionistic ATP systems and tools for converting the problems into ... about currently available ATP systems for intuitionistic logic and their performance results on the problems...

ICS
 Referenced in 20 articles
[sw21618]
 decision procedure for a fragment of firstorder logic. Terms are built from uninterpreted function...

FLOTTER
 Referenced in 16 articles
[sw29685]
 clause normal form translator for firstorder logic and a theorem prover for firstorder...

MUltlog
 Referenced in 19 articles
[sw06604]
 specification of a finitelyvalued firstorder logic and produces a sequent calculus, a natural...

CVC4
 Referenced in 108 articles
[sw09485]
 satisfiability) of firstorder formulas in a large number of builtin logical theories...

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

TeMP
 Referenced in 12 articles
[sw09989]
 TeMP: A temporal monodic prover. FirstOrder Temporal Logic ... FOTL, is an extension of classical firstorder logic by temporal operators for a discrete ... used model of time). Formulae of this logic are interpreted over structures that associate with ... representing a moment in time, a firstorder structure (D n ,I n ) with...

METEOR
 Referenced in 16 articles
[sw26327]
 reduce redundant search. However, research in logic programming has led to sophisticated architectures giving high ... linear input proof procedure for full firstorder logic, similar to but distinct from resolution...

FORS
 Referenced in 16 articles
[sw04848]
 combination of ILP and numerical regression. Firstorder logic descriptions are induced to carve...

PARTHEO
 Referenced in 15 articles
[sw09981]
 complete orparallel theorem prover for firstorder logic is presented. The proof calculus...

CoqHammer
 Referenced in 15 articles
[sw29396]
 with the translation of problems to the logics of automated systems and the reconstruction ... achieved for statements ”close to” firstorder logic and lemmas from the standard library...

HOLBoogie
 Referenced in 14 articles
[sw00409]
 enriched by annotations in firstorder logic.\parIts verification conditions  constructed via a wp calculus...

ArgoCLP
 Referenced in 12 articles
[sw07192]
 Coherent logic is a fragment of firstorder logic. The structure of the formulae...

FACTORIE
 Referenced in 13 articles
[sw08947]
 declarative language, such as SQL or firstorder logic, we advocate using an imperative language...

EDarvin
 Referenced in 19 articles
[sw06852]
 automated theorem prover for firstorder clausal logic with equality. It accepts problems in tptp...

EKRHyper
 Referenced in 12 articles
[sw21368]
 model generator and theorem prover for firstorder logic with equality. It implements...

Zapato
 Referenced in 11 articles
[sw25425]
 automatic theorem prover for quantifierfree firstorder logic helps to determine the feasibility...

Saturate
 Referenced in 10 articles
[sw21351]
 experimental theorem prover for firstorder logic, primarily based on saturation...