
CONOPT
 Referenced in 171 articles
[sw02791]
 constraints. The paper will discuss strategic and tactical decisions in the development, upgrade, and maintenance...

Isar
 Referenced in 145 articles
[sw04599]
 alternative proof language interface layer, beyond traditional tactic scripts. The Isabelle/Isar system provides an interpreter...

Sledgehammer
 Referenced in 138 articles
[sw07047]
 firstorder ATPs and builtin Isabelle tactics on a variety of benchmarks from Isabelle...

Matita
 Referenced in 72 articles
[sw06140]
 updating it according to commands (usually called tactics) issued by the user...

Mtac
 Referenced in 14 articles
[sw13075]
 Mtac: a monad for typed tactic programming in Coq. Effective support for custom proof automation ... development. However, existing languages for automation via tactics either (a) provide no way to specify ... behavior of tactics within the base logic of the accompanying theorem prover, or (b) rely ... extension to Coq that supports dependentlytyped tactic programming. Mtac tactics have access...

ArcAngel
 Referenced in 14 articles
[sw01812]
 ArcAngel: a tactic language for refinement. Morgan’s refinement calculus is a successful technique ... commonly used development strategies, documenting them as tactics, and using them as single transformation rules ... ArcAngel, a language for defining such refinement tactics; we present the language, its semantics ... laws. Apart from Angel, a generalpurpose tactic language that we are extending, no other...

MizarMode
 Referenced in 18 articles
[sw01973]
 Mizar is a nonprogrammable and nontactical verifier: the proofs are developed ... more laborious than the methods employed in tactical and programmable proof assistants, it makes...

KeYmaera X
 Referenced in 13 articles
[sw40558]
 KeYmaera X: an axiomatic tactical theorem prover for hybrid systems. KeYmaera X is a theorem ... specify custom proof search techniques as tactics, execute these tactics in parallel, and interface with ... Advanced proof search features—and userdefined tactics in particular—are difficult to check ... experiments suggest that a single layer of tactics on top of the prover kernel provides...

Irdis
 Referenced in 22 articles
[sw09690]
 idiom brackets; Indentation significant syntax; Extensible syntax; Tactic based theorem proving (influenced by Coq); Cumulative...

Paco
 Referenced in 22 articles
[sw10885]
 style constructions. The Paco library provides a tactic called ”pcofix”, replacing Coq’s primitive cofix...

SAP APO
 Referenced in 22 articles
[sw13389]
 following: Intercompany interaction on a strategic, tactical, and operative planning level; Collaboration with logistic partners...

Gappa
 Referenced in 19 articles
[sw04885]
 software verification plateform or as an automatic tactic for the Coq proof assistant...

Charge!
 Referenced in 10 articles
[sw22731]
 present a comprehensive set of tactics for working with a shallow embedding of a higher ... subset of Java in Coq. The tactics make it possible to reason at a level ... separationlogic proof outlines. In particular, the tactics allow the user to reason...

RACHET
 Referenced in 10 articles
[sw02342]
 Recursive Agglomeration of Clustering Hierarchies by Encircling Tactic) for analyzing multidimensional distributed data ... generated clustering hierarchies. RACHET employs the encircling tactic in which the merges at each stage...

Isabelle/UTP
 Referenced in 14 articles
[sw21184]
 obligations in the objectlanguage. Thirdly, proof tactics that transfer results from wellsupported mathematical...

Fiat
 Referenced in 14 articles
[sw21357]
 iteratively refined into efficient implementations via automated tactics. Each derivation in Fiat produces a formal...

VeriML
 Referenced in 8 articles
[sw13522]
 single language where users can develop complex tactics and decision procedures using a rich programming ... process, as users avoid developing domainspecific tactics and decision procedures.par In this paper ... showing a number of typesafe tactics and decision procedures written in VeriML...

Isabelle/Circus
 Referenced in 13 articles
[sw15208]
 proof rules from this semantics and implement tactic support that finally allows for proofs...

TacticToe
 Referenced in 6 articles
[sw28627]
 TacticToe: learning to reason with HOL4 tactics. Techniques combining machine learning with translation to automated ... traditional proof assistant automation as implemented by tactics and decision procedures. In this paper ... attempts to automate the selection of appropriate tactics and tacticsequences com bined with ... approach. We implement the technique as a tacticlevel automation for HOL4: TacticToe. It implements...

PRocH
 Referenced in 12 articles
[sw10191]
 firstorder theorem proving using the MESON tactic. The system is described and its performance...