Constructing infinite models represented by tree automata

DOI10.1007/s10472-009-9143-8zbMath1183.68562OpenAlexW2095271291MaRDI QIDQ1044230

Nicolas Peltier

Publication date: 11 December 2009

Published in: Annals of Mathematics and Artificial Intelligence (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10472-009-9143-8

zbMATH Keywords

finite model builders

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Mechanization of proofs and logical operations (03B35)

Uses Software

• MiniSat
• FINDER
• Mace4

Cites Work

• Unnamed Item
• Unnamed Item
• Predicting and detecting symmetries in FOL finite model search
• A structure-preserving clause form translation
• A method for simultaneous search for refutations and models by equational constraint solving
• Working with ARMs: Complexity results on atomic representations of Herbrand models
• Automated model building
• A new method for automated finite model building exploiting failures and symmetries
• Automated Deduction – CADE-20
• Automated Model Building: From Finite to Infinite Models

This page was built for publication: Constructing infinite models represented by tree automata