
TLPVS
 Referenced in 10 articles
[sw10024]
 linear temporal logic verification system. The system includes a set of theories defining a temporal ... which are particularly useful in a deductive ltl system. A distributed rank rule...

AFFIRM
 Referenced in 6 articles
[sw28906]
 theorem prover is an interative, naturaldeduction system centered around abstract data types. Since long...

Mcmt
 Referenced in 24 articles
[sw11911]
 declarative and deductive symbolic model checker for safety properties of infinite state systems whose state...

XcelLog
 Referenced in 4 articles
[sw13878]
 XcelLog: a deductive spreadsheet system. The promise of rulebased computing was to allow ... implementation of XcelLog, a usercentered deductive spreadsheet system, to empower nonprogrammers to specify ... based systems. The driving idea underlying the system is to treat sets as the fundamental ... indeed feasible to put the power of deductive spreadsheets for doing rulebased computing into...

InVeSt
 Referenced in 10 articles
[sw12034]
 invariance properties of infinite state systems. In VeSt integrates deductive and algorithmic verification principles...

SpatialYap
 Referenced in 2 articles
[sw13884]
 LogicBased Geographic Information System. Coupled deductive database systems join together logic programming systems ... seen the evolution of relational database management systems in order to enable them to store ... describe the application of the MYDDAS deductive database system to the handling of spatial data ... order to obtain a spatial deductive database system, that can be used as a geographic...

Ivy
 Referenced in 10 articles
[sw41668]
 parameterized and infinitestate systems via three modes: deductive verification using an SMT solver, abstraction...

Symlog
 Referenced in 3 articles
[sw32623]
 Fitchstyle proof construction. Symlog is a system for learning symbolic logic by computer ... formal proofs in Fitchstyle natural deduction systems of propositional and predicate logic...

PLM
 Referenced in 3 articles
[sw38031]
 construct an implementation of the deductive system of PLM which allows to automatically and interactively...

ASTRA
 Referenced in 12 articles
[sw00052]
 formalised deductive technique allowing the investigation of possible causes of undesired system states, referred...

KIDS
 Referenced in 12 articles
[sw15441]
 described. The system has components for performing algorithm design, deductive inference, program simplification, partial evaluation ... programs have been derived using the system, and it is believed that KIDS could...

PTTP+GLiDeS
 Referenced in 2 articles
[sw30126]
 System Description: PTTP+GLiDeS Semantically Guided PTTP. PTTP+GLiDeS is a semantically guided linear deduction ... OTTER and is a forward chaining resolution system; CLINS [3] uses hyperlinking; RAMCS ... chain format linear deduction system based on Graph Construction. Of these, CLINS and SGLD...

TAS
 Referenced in 11 articles
[sw04900]
 logic. Our transformation system TAS compiles these rules to concrete deduction support, complete with...

ALISA
 Referenced in 5 articles
[sw03031]
 Automatic deductive synthesis of Lisp programs in the system ALISA...

DrawCAD
 Referenced in 2 articles
[sw01611]
 references to the other objects they contain. Deductive objectrelational databases can be used ... idea behind the development of the DrawCAD system. DrawCAD is a CAD system built ... Relationlog objectrelational deductive database system. It facilitates the creation of graphical objects by reusing ... system illustrates how CAD systems can be developed, using deductive objectrelational databases to store...

IMPS
 Referenced in 52 articles
[sw09143]
 system. IMPS is an interactive mathematical proof system intended as a generalpurpose tool ... steps to facilitate human control of the deductive process and human comprehension of the resulting...

MYDDAS
 Referenced in 3 articles
[sw13885]
 development of a highly efficient deductive database system, based on the coupling of the MySQL...

Celf
 Referenced in 2 articles
[sw22718]
 Celf  a logical framework for deductive and concurrent systems. (System description). CLF (Concurrent ... framework for specifying and implementing deductive and concurrent systems from areas, such as programming language...

MikiBeta
 Referenced in 1 article
[sw09920]
 well as a simple deduction system for Combinatory Logic...

KEIM
 Referenced in 1 article
[sw19608]
 KEIM: A toolkit for automated deduction. KEIM is a collection of software modules, written ... used in the implementation of automated reasoning systems. KEIM is intended to be used ... want to build or use deduction systems (such as resolution theorem provers) without having ... substitutions; proofs, including resolution and natural deduction styles...