• CONOPT

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

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

  • Referenced in 138 articles [sw07047]
  • first-order ATPs and built-in Isabelle tactics on a variety of benchmarks from Isabelle...
  • Matita

  • Referenced in 71 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 dependently-typed 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 general-purpose tactic language that we are extending, no other...
  • MizarMode

  • Referenced in 18 articles [sw01973]
  • Mizar is a non-programmable and non-tactical verifier: the proofs are developed ... more laborious than the methods employed in tactical and programmable proof assistants, it makes...
  • 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 18 articles [sw04885]
  • software verification plateform or as an automatic tactic for the Coq proof assistant...
  • KeYmaera X

  • Referenced in 9 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 user-defined tactics in particular—are difficult to check ... experiments suggest that a single layer of tactics on top of the prover kernel provides...
  • 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 ... separation-logic 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 multi-dimensional 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 object-language. Thirdly, proof tactics that transfer results from well-supported 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 domain-specific tactics and decision procedures.par In this paper ... showing a number of type-safe 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 tactic-sequences com- bined with ... approach. We implement the technique as a tactic-level automation for HOL4: TacticToe. It implements...
  • PRocH

  • Referenced in 12 articles [sw10191]
  • first-order theorem proving using the MESON tactic. The system is described and its performance...