cvc5.git - CVC4 is an efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems.

Age	Commit message (Collapse)	Author
2020-05-26	(proof-new) Update proof checker. (#4511)	Andrew Reynolds
	This adds new required features to proof checker and the base class of proof rule checker. This is required as the first dependency towards merging further infrastructure related to proofs.
2020-04-20	Add SCOPE proof rule (#4332)	Andrew Reynolds
	This rule is dual to ASSUME. It is a way of closing free assumptions to conclude an implication. It also changes getId -> getRule.
2020-04-16	Add ProofNodeManager and ProofChecker (#4317)	Andrew Reynolds
	Further work on adding core utilities for ProofNode objects, in support of the new proof infrastructure. ProofNodeManager is analogous to NodeManager. It is a trusted way of generating only "well-formed" ProofNode pointers (according to a checker). ProofChecker is analogous to TypeChecker. It is intended to be infrastructure for our internal proof checker. This PR (and 1 more) is required to get to a place where Haniel and I can collaborate on further development for proofs.