
Isar
 Referenced in 145 articles
[sw04599]
 examples of this kind of semiautomated reasoning systems include Coq, PVS, HOL, and Isabelle ... Paradoxically, none of the existing semiautomated reasoning systems have an adequate primary notion ... just maintenance). The Intelligible semiautomated reasoning (Isar) approach to readable formal proof documents sets ... logic, and integrates a broad range of automated proof methods. Interactive proof development is supported...

LCF
 Referenced in 158 articles
[sw08360]
 form a thriving paradigm in computer assisted reasoning. Many of the developments of the last ... uence on the ¯eld of automated reasoning has been diverse and profound...

NQTHM
 Referenced in 151 articles
[sw07543]
 logic and its theorem prover” [J. Autom. Reasoning 4, No.2, 117172 (1988)]. However...

MaLARea
 Referenced in 50 articles
[sw10278]
 MaLARea: a Metasystem for Automated Reasoning in Large Theories. MaLARea (a Machine Learner for Automated ... simple metasystem iteratively combining deductive Automated Reasoning tools (now the E and the SPASS...

RRL
 Referenced in 55 articles
[sw28904]
 environment for experimenting with automated reasoning algorithms for equational logic based on rewrite techniques ... hard and challenging mathematical problems in automated reasoning literature as well as a research tool...

GEX
 Referenced in 35 articles
[sw09961]
 various mathematical concepts. As an automated reasoning software, we can build dynamic logic models which ... most of the effective methods for geometric reasoning introduced in the past twenty years, including ... angle method. With these methods, users may automated prove geometry theorems, to discover new prrperties...

HR
 Referenced in 29 articles
[sw10392]
 applications of HR to automated reasoning include the generation of constraints for constraint satisfaction problems ... generation of lemmas for automated theorem proving, and the production of benchmark theorems...

MetaPRL
 Referenced in 26 articles
[sw04624]
 with support for interactive proof and automated reasoning. A primary feature of MetaPRL...

MathWeb
 Referenced in 18 articles
[sw10293]
 MathWeb software bus for distributed mathematical reasoning. Automated reasoning systems have reached a high degree ... last decade. Many reasoning tasks can be delegated to an automated theorem prover ... people other than their own developers. The reasons for this seem to be that...

HOLyHammer
 Referenced in 26 articles
[sw11553]
 that, the service uses several automated reasoning systems combined with several premise selection methods trained...

RSat
 Referenced in 22 articles
[sw13117]
 RSat is developed by the UCLA Automated Reasoning Group...

dedukti
 Referenced in 19 articles
[sw13663]
 Kirchner, Theorem proving modulo, Journal of Automated Reasoning...

SamIam
 Referenced in 17 articles
[sw29886]
 networks, developed in Java by the Automated Reasoning Group of Professor Adnan Darwiche at UCLA...

CoqHammer
 Referenced in 17 articles
[sw29396]
 CoqHammer is a generalpurpose automated reasoning hammer tool for Coq. It combines learning from ... translation of problems to the logics of automated systems and the reconstruction of successfully found...

Sparkle
 Referenced in 14 articles
[sw09803]
 based on lazy graphrewriting. This allows reasoning to take place on the program itself ... uses di.erent concepts. Secondly, Sparkle supports automated reasoning. Trivial goals will automatically be discarded...

SRASS
 Referenced in 12 articles
[sw21370]
 solved alone by the underlying conventional automated reasoning system...

ETPS
 Referenced in 161 articles
[sw06302]
 proving include hardware and software verification, partial automation of various mathematical activities, promoting development ... these disciplines, expert systems which can reason, and certain aspects of artificial intelligence...

VeriFun
 Referenced in 10 articles
[sw22187]
 VeriFun is a reasoning system for verification of statements about programs written in a simple ... easy to use system for teaching Automated Reasoning, Semantics, Verification and similar subjects...

Ivy
 Referenced in 10 articles
[sw41668]
 designed to support decidable automated reasoning, to improve proof stability and to provide transparency...

MMP/Geometer
 Referenced in 14 articles
[sw00584]
 MMP/Geometer – a software package for automated geometric reasoning. We introduce a software package, MMP/Geometer, developed...