
QMLTP
 Referenced in 8 articles
[sw09915]
 problem library for firstorder modal logics. The Quantified Modal Logic Theorem Proving (QMLTP) library ... theorem proving (ATP) systems for firstorder modal logics. The main purpose of the library...

MleanCoP
 Referenced in 6 articles
[sw21522]
 MleanCoP: a connection prover for firstorder modal logic. MleanCoP is a fully automated theorem ... prover for firstorder modal logic. The proof search is based on a prefixed connection...

MSPASS
 Referenced in 24 articles
[sw17667]
 firstorder theorem prover spass, which can be used as a modal logic theorem prover...

FMLtoHOL
 Referenced in 3 articles
[sw21539]
 based firstorder modal logic provers. Firstorder modal logics (FMLs) can be modeled...

SQEMA
 Referenced in 38 articles
[sw03056]
 Algorithmic correspondence and completeness in modal logic. IV. Semantic extensions of SQEMA ... SQEMA for computing firstorder equivalents and proving canonicity of modal formulae, and thus established...

ModLeanTAP
 Referenced in 18 articles
[sw12368]
 modular labelled tableau calculus for propositional modal logics (where the labels contain free and universal ... modal deduction. ModLeanTAP’s development was inspired by the lean tableaubased prover for first ... order logic leanTAP. ModLeanTAP Version 2.0 includes additional search space restrictions and fairness strategies, giving...

HyLoRes
 Referenced in 7 articles
[sw17660]
 modal (or hybrid) input, with no translation into background logics ... HyLoRes fuses stateoftheart firstorder proving ideas with the simple representation...

SOLOIST
 Referenced in 1 article
[sw16438]
 manysorted firstorder metric temporal logic, extended with new temporal modalities that support aggregate...

MGTP
 Referenced in 7 articles
[sw09701]
 generation based theorem prover MGTP for firstorder logic. This paper describes the major results ... negation as failure, abductive reasoning and modal logic systems, on MGTP. These techniques share...

iCTRL
 Referenced in 1 article
[sw01473]
 natural language texts. Traditional firstorder and intensional logic cannot cope with numerous natural language ... phenomena such as the large variety of modalities, satisfactory interpretation of iterative application of modal...

ANSYS
 Referenced in 662 articles
[sw00044]
 ANSYS offers a comprehensive software suite that spans...

Coq
 Referenced in 1807 articles
[sw00161]
 Coq is a formal proof management system. It...

Dafny
 Referenced in 66 articles
[sw00183]
 Dafny is an imperative objectbased language with...

Isabelle
 Referenced in 611 articles
[sw00454]
 Isabelle is a generic proof assistant. It allows...

LEOII
 Referenced in 51 articles
[sw00512]
 LEOII is a standalone, resolutionbased higher...

Maple
 Referenced in 5124 articles
[sw00545]
 The result of over 30 years of cutting...

Mathematica
 Referenced in 5957 articles
[sw00554]
 Almost any workflow involves computing results, and that...

Matlab
 Referenced in 12309 articles
[sw00558]
 MATLAB® is a highlevel language and interactive...

MiniSat
 Referenced in 536 articles
[sw00577]
 An extensible SATsolver. MiniSat is a minimalistic...

Nitpick
 Referenced in 61 articles
[sw00622]
 Nitpick is a counterexample generator for Isabelle/HOL that...