PackagesReroutesAboutlamdera.com

logicUSLIB/logicus-fol/3.1.0

NOTE: the latest version is 3.3.0

READMEAboutVersionsSourceModules

LogicUS.FOL.ToStringP9M4

Translation of formulas to the syntax of Prover9 and Mace4.

Deprecated: use LogicUS.FOL.Prover9Mace4, which builds the whole input file with readable symbol names and reads Mace4 models back. This module is kept for compatibility.

It translates a formula to Prover9/Mace4 syntax, renaming predicates, functions, constants and variables to P0, f0, c0, A, B... (Deprecated.)

-> { vi : Int
, vdic : Dict Variable Int
, pi : Int
, pdic : Dict Ident Int
, fi : Int
, fdic : Dict Ident Int
, ci : Int
, cdic : Dict Ident Int
}
-> ( String
, { vi : Int
, vdic : Dict Variable Int
, pi : Int
, pdic : Dict Ident Int
, fi : Int
, fdic : Dict Ident Int
, ci : Int
, cdic : Dict Ident Int
}
)

Like ffol2P9M4Str, but it receives and returns the renaming tables. (Deprecated.)

sfol2P9M4Str : SetFOL -> String

It translates a set of formulas to Prover9/Mace4 syntax, one per line, with the same renaming as ffol2P9M4Str. (Deprecated.)

-> { vi : Int
, vdic : Dict Variable Int
, pi : Int
, pdic : Dict Ident Int
, fi : Int
, fdic : Dict Ident Int
, ci : Int
, cdic : Dict Ident Int
}
-> ( String
, { vi : Int
, vdic : Dict Variable Int
, pi : Int
, pdic : Dict Ident Int
, fi : Int
, fdic : Dict Ident Int
, ci : Int
, cdic : Dict Ident Int
}
)

Like sfol2P9M4Str, but it receives and returns the renaming tables, so several sets can share them. (Deprecated.)

It translates a formula to Prover9/Mace4 syntax keeping the symbol names between quotes. (Deprecated.)

sfol2P9M4StrUnsafe : SetFOL -> String

It translates a set of formulas to Prover9/Mace4 syntax keeping the symbol names between quotes. (Deprecated.)

Modules

About this package serverReroutesreroutes.json
Pages and docs rendering from package.elm-lang.org, © 2012-2020 Evan Czaplicki. © 2026 Lamdera