
Z
 Referenced in 282 articles
[sw10291]
 with the exception of the natural deduction calculus, see below  only introduction ... broad and tedious exposition of the natural deduction calculus, which is not used further...

ETPS
 Referenced in 160 articles
[sw06302]
 theories in a wide variety of disciplines, deductive information systems for these disciplines, expert systems ... expansion proofs, translating these into natural deduction proofs, constructing natural deduction proofs, translating natural deduction ... interactive facilities of TPS for constructing natural deduction proofs have been used under the name...

TPS
 Referenced in 73 articles
[sw00973]
 theories in a wide variety of disciplines, deductive information systems for these disciplines, expert systems ... expansion proofs, translating these into natural deduction proofs, constructing natural deduction proofs, translating natural deduction...

LEGO
 Referenced in 107 articles
[sw09685]
 interactive proof development in the natural deduction style. It supports refinement proof as a basic...

TRAMP
 Referenced in 21 articles
[sw21343]
 Transformation of MachineFound Proofs into Natural Deduction Proofs at the Assertion Level. The Tramp ... first order logic with equality into natural deduction proofs at the assertion level. Through this...

MUltlog
 Referenced in 19 articles
[sw06604]
 produces a sequent calculus, a natural deduction system, and clause formation rules for this logic...

Pandora
 Referenced in 9 articles
[sw01306]
 Pandora (Proof Assistant for Natural Deduction using Organised Rectangular Areas) is a learning support tool ... designed to guide the construction of natural deduction proofs...

Ivy
 Referenced in 9 articles
[sw41668]
 model checking, and manual proofs using natural deduction. It supports lightweight formal methods...

AFFIRM
 Referenced in 6 articles
[sw28906]
 AFFIRM theorem prover is an interative, naturaldeduction system centered around abstract data types. Since...

FOL Fitting
 Referenced in 5 articles
[sw28611]
 semantics, the model existence theorem, a natural deduction proof calculus together with a proof...

Psyche
 Referenced in 5 articles
[sw28518]
 inference rules of the logic in natural deduction: it uses instead a focused sequent calculus...

PROVERB
 Referenced in 4 articles
[sw29672]
 abstracts machinefound proofs to natural deduction style proofs at an adequate level of abstraction...

KeYmaera
 Referenced in 44 articles
[sw03709]
 verification tool for hybrid systems that combines deductive, real algebraic, and computer algebraic prover technologies ... automated and interactive theorem prover for a natural specification and verification logic for hybrid systems...

Symlog
 Referenced in 3 articles
[sw32623]
 formal proofs in Fitchstyle natural deduction systems of propositional and predicate logic...

ANDP
 Referenced in 1 article
[sw29686]
 Automated natural deduction prover and experiments. The paper presents the heuristics and techniques which ... used to implement automated natural deduction prover (ANDP), the natural deduction was adapted from Gentzen...

GCLC
 Referenced in 31 articles
[sw00326]
 storing mathematical contents of visual nature in textual form. In GCLC, there is a build ... links visual and semantical geometrical information with deductive properties and machinegenerated proofs...

Delphin
 Referenced in 18 articles
[sw21365]
 Delphin: Functional programming with deductive systems. We present the design and implementation of the strict ... proofs and typing derivations in a natural and intuitive...

KEIM
 Referenced in 1 article
[sw19608]
 those who want to build or use deduction systems (such as resolution theorem provers) without ... substitutions; proofs, including resolution and natural deduction styles...

TILT
 Referenced in 1 article
[sw24052]
 term represents a proof in the natural deduction calculus. Since the search space...