In proof complexity, a Frege system is a propositional proof system whose proofs are sequences of formulas derived using a finite set of sound and implicationally complete inference rules.[1] Frege systems (more often known as Hilbert systems in general proof theory) are named after Gottlob Frege.
The name "Frege system" was first defined[2] by Stephen Cook and Robert Reckhow,[3][4] and was intended to capture the properties of the most common propositional proof systems.[2]
- ^ Krajicek, Jan (1995-11-24). Bounded Arithmetic, Propositional Logic and Complexity Theory. Cambridge University Press. p. 42. ISBN 978-0-521-45205-2.
- ^ a b Pudlák, Pavel; Buss, Samuel R. (1995). "How to lie without being (easily) convicted and the lengths of proofs in propositional calculus". In Pacholski, Leszek; Tiuryn, Jerzy (eds.). Computer Science Logic. Lecture Notes in Computer Science. Vol. 933. Berlin, Heidelberg: Springer. pp. 151–162. doi:10.1007/BFb0022253. ISBN 978-3-540-49404-1.
- ^ Cook, Stephen; Reckhow, Robert (1974-04-30). "On the lengths of proofs in the propositional calculus (Preliminary Version)". Proceedings of the sixth annual ACM symposium on Theory of computing - STOC '74. New York, NY, USA: Association for Computing Machinery. pp. 135–148. doi:10.1145/800119.803893. ISBN 978-1-4503-7423-1.
- ^ Cook, Stephen A.; Reckhow, Robert A. (1979). "The relative efficiency of propositional proof systems". The Journal of Symbolic Logic. 44 (1): 36–50. doi:10.2307/2273702. ISSN 0022-4812. JSTOR 2273702.