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

REDLOG
 Referenced in 166 articles
[sw04250]
 manipulation of firstorder formulas over some temporarily fixed language and theory. In contrast...

Boolector
 Referenced in 32 articles
[sw00085]
 vectors and arrays. Satisfiability Modulo Theories (SMT) is the problem of deciding satisfiability ... formula, expressed in a combination of firstorder theories. We present the architecture and selected...

CVC4
 Referenced in 125 articles
[sw09485]
 source automatic theorem prover for satisfiability modulo theories (SMT) problems. It can be used ... firstorder formulas in a large number of builtin logical theories and their combination...

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

FOCI
 Referenced in 62 articles
[sw12868]
 quantifierfree firstorder formulas. It supports certain interpreted theories, such as equality, uninterpreted functions...

OTTER
 Referenced in 320 articles
[sw02904]
 designed to prove theorems stated in firstorder logic with equality. Otter’s inference rules ... includes facilities for term rewriting, term orderings, KnuthBendix completion, weighting, and strategies for directing ... Boolean algebra, logic calculi, combinatory logic, group theory, lattice theory, and algebraic geometry. Note: Otter/Mace2...

f2lp
 Referenced in 10 articles
[sw09898]
 certain conditions, system f2lp turns a firstorder theory under the stable model semantics into...

LPTP
 Referenced in 7 articles
[sw01822]
 pure Prolog programs. This is a firstorder theory that contains induction principles corresponding...

CoqMTU
 Referenced in 3 articles
[sw19138]
 universes parametrized by a decidable firstorder theory. e study a complex type theory ... predicative hierarchy of universes and a firstorder theory T built in its conversion relation ... theory T is specified abstractly, by a set of constructors, a set of defined symbols ... principle relying on crucial properties of firstorder structures satisfying the axioms. We first show...

FOIL
 Referenced in 31 articles
[sw24694]
 firstorder learning system that uses information in a collection of relations to construct theories...

CoqMT
 Referenced in 6 articles
[sw19139]
 Modulo Theory. Coq Modulo Theory (CoqMT) is an extension of the Coq proof assistant incorporating ... validity entailment for userdefined firstorder equational theories. Such a mechanism strictly enriches ... checking algorithm and the integration of firstorder decision procedures. We present here CoqMT...

anthem
 Referenced in 4 articles
[sw30423]
 anthem: Transforming gringo Programs into FirstOrder Theories (Preliminary Report). In a recent paper...

Nitpick
 Referenced in 64 articles
[sw00622]
 builds on Kodkod, a SATbased firstorder relational model finder. Nitpick supports unbounded quantification ... card system. Our experimental results on Isabelle theories and the TPTP library indicate that Nitpick...

FORT
 Referenced in 2 articles
[sw28637]
 tool that implements the firstorder theory of rewriting for the decidable class of left ... satisfy arbitrary properties expressible in the firstorder theory of rewriting. In this paper...

TSAT++
 Referenced in 3 articles
[sw21350]
 lazy SATbased approach to satisfiability modulo theories (SMT). SMT is the problem of determining ... literals, where T is a firstorder theory for which a satisfiability procedure...

PrASP
 Referenced in 3 articles
[sw18512]
 reasoning based on logic programming and firstorder theories under stable model semantics. This system ... AnsProlog) as well as firstorder logic formulas (with stable model semantics), annotated with conditional...

AGES
 Referenced in 3 articles
[sw32284]
 automatically generate models for ordersorted firstorder theories. The tool uses linear algebra techniques...

AVATAR
 Referenced in 21 articles
[sw28636]
 firstorder resolution and superposition theorem provers called AVATAR (Advanced Vampire Architecture for Theories...

Mcmt
 Referenced in 24 articles
[sw11911]
 state systems whose state variables are arrays. Theories specify the properties of the indexes ... system are described by quantified firstorder formulae. The core of the system ... points by solving Satisfiability Modulo Theories (SMT) problems. Besides standard SMT techniques, efficient heuristics...