Uses of Interface
dev.civl.sarl.prove.IF.TheoremProverFactory
Packages that use TheoremProverFactory
Package
Description
Module "prove" constitutes the interface between SARL and (possibly external)
theorem provers.
The internal interface for the "reason" module, which deals with
Reasoners --- objects used to prove
theorems and simplify symbolic expressions.-
Uses of TheoremProverFactory in dev.civl.sarl.prove.IF
Methods in dev.civl.sarl.prove.IF that return TheoremProverFactoryModifier and TypeMethodDescriptionstatic TheoremProverFactoryProve.newMultiProverFactory(PreUniverse universe, SARLConfig config, Path workingDirectory) Constructs a new theorem prover factory based on the given configuration.static TheoremProverFactoryProve.newProverFactory(PreUniverse universe, ProverInfo prover, Path workingDirectory) Constructs a new theorem prover factory based on a single underlying theorem prover.static TheoremProverFactoryProve.trivialProverFactory() -
Uses of TheoremProverFactory in dev.civl.sarl.reason.IF
Methods in dev.civl.sarl.reason.IF with parameters of type TheoremProverFactoryModifier and TypeMethodDescriptionstatic ReasonerFactoryReason.newReasonerFactory(PreUniverse universe, IdealFactory idealFactory, TheoremProverFactory proverFactory) Create a reasoner factory