coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] FOL or SOL formalization in Coq

From: Francisco Trucco <franciscoctrucco AT gmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] FOL or SOL formalization in Coq
Date: Mon, 17 Dec 2018 12:39:13 -0300
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=franciscoctrucco AT gmail.com; spf=Pass smtp.mailfrom=franciscoctrucco AT gmail.com; spf=None smtp.helo=postmaster AT mail-yw1-f41.google.com
Ironport-phdr: 9a23:RAM44RzCJ7kJ29nXCy+O+j09IxM/srCxBDY+r6Qd1OwfIJqq85mqBkHD//Il1AaPAd2Lraocw8Pt8InYEVQa5piAtH1QOLdtbDQizfssogo7HcSeAlf6JvO5JwYzHcBFSUM3tyrjaRsdF8nxfUDdrWOv5jAOBBr/KRB1JuPoEYLOksi7ze+/94HQbglSmDaxfa55IQmrownWqsQYm5ZpJLwryhvOrHtIeuBWyn1tKFmOgRvy5dq+8YB6/ShItP0v68BPUaPhf6QlVrNYFygpM3o05MLwqxbOSxaE62YGXWUXlhpIBBXF7A3/U5zsvCb2qvZx1S+HNsDwULs6Wymt771zRRDniCkJOT03/nzJhMNsl69Uug6tqgZlzoLIfI2YNvxzdb7dc9MAQmpBW95cWSxbAoymaYsAE+sBPf1EoIn6ulAAswG+BRSwC+zzzT9Dm3j73aMg0+s7FwHJwA0gH8kSv3TTsNr1KL0SUf2pw6bUyjXOdPxW2TLn54jJdhAtu+2DXbV1ccfIz0QkCg3LjlKVqYP/PjOV0PwAs2ea7+p8VeKvlnUopxttrTiow8chjJTCiIENyl3c6yl13II4Kce7RUN7e9KoDZpduzyAO4Z5X88vRXxjtjwgxb0co5G7eTAHyJQ5yB7bbPyKa42I7QjiVOaVODt5hHxkdK+mixa8/kWs1/fwVsaz0FZNoSpFlsfDumoR2BzU78iLUvp9/kG/1jaTzw3f9P1ILEQumafYK5Mt2KM8m5sOvUjZESL6hV36jKqMeUUl/uio5f7nYrLjppKEOY90kBvxMqIylcy+GuQ3Lg8OUHSH+eSmyb3s4VH2QLJRg/05l6nWqpHaJcABqqGlBA9V154v6wyjADe+zNQYgX4HIUpZdxKAlojlIk3BIPTlDfikmFmsizdqx/XePrL7GJnNL37DkK3gfbln8UJcxhAznphj4MdfDahEK/buUGfwssbZB1k3KV+a2eHiXftn34UVWHmEBeelKr7ZuljAsuw1Ku+HZZQevz3hMeUu7PnGgnowmFtbdq6si8hEIEukF+hrdh3KKUHnhc0MRD9T71gOCdfygVjHagZ9InO7XqYy/DY+Udv0AoLKR4Tri7uEjn7iQs9mI1teA1XJKk/GMp2eUq5VOi2XK85l1DcDUOr5EtJz5VSVrAb/joFfAK/U9ykf78+x0dF046jCikh3+2AtScua1G6JQid/mWZaHzI=

Hi all,

I was wondering if any of you knew of a first order logic or second order logic formalization in Coq. In particular, I am looking for something similar to Coq in Coq but with FOL or SOL.

Thanks a lot!

Francisco Trucco

[Coq-Club] FOL or SOL formalization in Coq, Francisco Trucco, 12/17/2018
- Re: [Coq-Club] FOL or SOL formalization in Coq, roux cody, 12/17/2018
  - Re: [Coq-Club] FOL or SOL formalization in Coq, Milad Ketabii, 12/17/2018
- Re: [Coq-Club] FOL or SOL formalization in Coq, Yannick Forster, 12/17/2018