Full first-order free variable sequents and tableaux in implicit induction

DOI10.1007/3-540-48754-9_25MaRDI QIDQ4263022zbMATH OpenFDO

Authors Claus-Peter Wirth

Publication date 28 February 2000

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-48754-9_25

zbMATH Keywords

free variable calculiimplicit inductive theorem provingsequent calculitableau calculi

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• Full first-order sequent and tableau calculi with preservation of solutions and the liberalized -rule but without Skolemization
• scientific article; zbMATH DE number 1552522
• Lean induction principles for tableaux
• Types for Proofs and Programs

Cited in

(5)

• Free-variable tableaux for monotonic preorders
• Free variable tableaux for a logic with term declarations
• Full first-order sequent and tableau calculi with preservation of solutions and the liberalized -rule but without Skolemization
• Lean induction principles for tableaux
• A free variable sequent calculus with uniform variable splitting

This page was built for publication: Full first-order free variable sequents and tableaux in implicit induction

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4263022)