caa a22 4500 475797469 CHVBK 20180406123728.0 cr unu---uuuuu 170329e20000101xx s 000 0 eng 10.1023/A:1008725524946 doi (NATIONALLICENCE)springer-10.1023/A:1008725524946 A Tutorial on Stålmarck's Proof Procedure for Propositional Logic [Elektronische Daten] [Mary Sheeran, Gunnar Stålmarck] We explain Stålmarck's proof procedure for classical propositional logic. The method is implemented in a commercial tool that has been used successfully in real industrial verification projects. Here, we present the proof system underlying the method, and motivate the various design decisions that have resulted in a system that copes well with the large formulas encountered in industrial-scale verification. Kluwer Academic Publishers, 2000 propositional logic (Boolean logic) nationallicence tautology checking (propositional theorem proving) nationallicence Dilemma proof system nationallicence k-saturation nationallicence proof depth nationallicence tautological hardness nationallicence proof complexity nationallicence industrial applications of formal methods nationallicence Sheeran Mary Prover Technology AB and Chalmers University of Technology, Sweden aut Stålmarck Gunnar Prover Technology AB and Chalmers University of Technology, Sweden aut Formal Methods in System Design Kluwer Academic Publishers 16/1(2000-01-01), 23-58 0925-9856 16:1<23 2000 16 10703 https://doi.org/10.1023/A:1008725524946 text/html Onlinezugriff via DOI 1 research-article jats NATIONALLICENCE 856 40 https://doi.org/10.1023/A:1008725524946 text/html Onlinezugriff via DOI NATIONALLICENCE 700 1- Sheeran Mary Prover Technology AB and Chalmers University of Technology, Sweden aut NATIONALLICENCE 700 1- Stålmarck Gunnar Prover Technology AB and Chalmers University of Technology, Sweden aut NATIONALLICENCE 773 0- Formal Methods in System Design Kluwer Academic Publishers 16/1(2000-01-01), 23-58 0925-9856 16:1<23 2000 16 10703 Metadata rights reserved Springer special CC-BY-NC licence nationallicence BK010053 XK010053 XK010000 NATIONALLICENCE NATIONALLICENCE NL-springer