content/tools/sat-smt/zipperposition.md

+++ date = 2025-06-07 draft = false title = 'Zipperposition' subtitle = 'Theorem Prover' links = [ { title = "Homepage", url = "https://sneeuwballen.github.io/zipperposition/", icon = 'fa-solid fa-home' }, { title = "Source Code", url = "https://github.com/sneeuwballen/zipperposition", icon = 'fa-brands fa-github' }, # { title = "Playground", url = "https://jfmc.github.io/z3-play/", icon = 'fa-solid fa-gamepad' } ] applications = ['Theorem Prover'] developers = ['TU Wien'] licenses = ['BSD']

inputs = ['']

interfaces = ['CLI'] maintenance = ['Actively Maintained']

techniques = ['CDCL']

publications = ['deMoura2008']

+++

Zipperposition is an automated theorem prover for first-order logic with equality and theories.